coq: update key bindings and README

README: - add `SPC m` prefixes to follow the style of the other READMEs - Sort key bindings alphabetically Key bindings changes made to be more mnemocnic and/or to better fit the other key bindings of other layers: - SPC m p b --> SPC m p p (show prover process buffer) - SPC m p c --> SPC m p i (interrupt prover process) - SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would be better ?) - SPC m a p --> SPC m a a to print query - SPC m a n p --> SPC m a A to print query showing all - SPC m a i p --> SPC m a i i to print query showing implicits - Ask showing all bindings use the same keys as regular Ask but the last key is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about showing all) - Ask showing implicits are still on SPC m a i (we could also use Control key, for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit), it depends on how frequent showing implicits are used). - SPC m g . --> SPC m g l (go to end of Locked command) - SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs) - SPC m g a --> SPC m g s (to go to start of command)
syl20bnr · Feb 13, 2017 · fe168f0 · fe168f0
1 parent 8b72130
commit fe168f0
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 51 deletions.
diff --git a/layers/+lang/coq/README.org b/layers/+lang/coq/README.org
@@ -32,60 +32,58 @@ Official installers for MacOS and Windows are available from:
 Linux users can build from source or consult with their own package managers.
 
 * Key bindings
-All Coq specific bindings are prefixed with the major-mode leader ~SPC m~.
-
 ** Laying out windows
 
 | Key Binding | Description           |
 |-------------+-----------------------|
-| ~ll~        | Re-layout windows     |
-| ~lc~        | Clear response buffer |
-| ~lp~        | Show current proof    |
+| ~SPC m l c~ | Clear response buffer |
+| ~SPC m l l~ | Re-layout windows     |
+| ~SPC m l p~ | Show current proof    |
 
 ** Managing prover process
 
 | Key Binding | Description                                                     |
 |-------------+-----------------------------------------------------------------|
-| ~pc~        | Interrupt prover                                                |
-| ~px~        | Quit prover                                                     |
-| ~pr~        | Retract buffer - rewinds and moves point to beginning of buffer |
-| ~pb~        | Process buffer - processes and moves point to end of buffer     |
+| ~SPC m p i~ | Interrupt prover                                                |
+| ~SPC m p p~ | Process buffer - processes and moves point to end of buffer     |
+| ~SPC m p q~ | Quit prover                                                     |
+| ~SPC m p r~ | Retract buffer - rewinds and moves point to beginning of buffer |
 
 ** Prover queries
 The mnemonic for =a= is "ask".
 
-| Key Binding | Description                                 |
-|-------------+---------------------------------------------|
-| ~af~        | Search (mnemonic: "find theorems")          |
-| ~ao~        | Show an outline of the current proof script |
-| ~ap~        | Print                                       |
-| ~ac~        | Check                                       |
-| ~ab~        | About                                       |
-| ~aip~       | Print (showing implicits)                   |
-| ~aic~       | Check (showing implicits)                   |
-| ~aib~       | About (showing implicits)                   |
-| ~anp~       | Print (showing all)                         |
-| ~anc~       | Check (showing all)                         |
-| ~anb~       | About (showing all)                         |
+| Key Binding   | Description                                 |
+|---------------+---------------------------------------------|
+| ~SPC m a a~   | Print                                       |
+| ~SPC m a A~   | Print (showing all)                         |
+| ~SPC m a b~   | About                                       |
+| ~SPC m a B~   | About (showing all)                         |
+| ~SPC m a c~   | Check                                       |
+| ~SPC m a C~   | Check (showing all)                         |
+| ~SPC m a f~   | Search (mnemonic: "find theorems")          |
+| ~SPC m a i b~ | About (showing implicits)                   |
+| ~SPC m a i c~ | Check (showing implicits)                   |
+| ~SPC m a i i~ | Print (showing implicits)                   |
+| ~SPC m a o~   | Show an outline of the current proof script |
 
 ** Moving the point
 
 | Key Binding | Description                     |
 |-------------+---------------------------------|
-| ~g.~        | Go to last processed command    |
-| ~ga~        | Go to start of command at point |
-| ~ge~        | Go to end of command at point   |
-| ~gd~        | Go to definition at point       |
+| ~SPC m g e~ | Go to end of command at point   |
+| ~SPC m g g~ | Go to definition at point       |
+| ~SPC m g l~ | Go to last processed command    |
+| ~SPC m g s~ | Go to start of command at point |
 
 ** Inserting
 
-| Key Binding | Description                                                     |
-|-------------+-----------------------------------------------------------------|
-| ~il~        | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
-| ~im~        | Insert =match= on a type                                        |
-| ~ie~        | Insert =End <section-name>=                                     |
-| ~M-RET~     | Insert regular match branch                                     |
-| ~M-S-RET~   | Insert =match goal with= branch                                 |
+| Key Binding     | Description                                                     |
+|-----------------+-----------------------------------------------------------------|
+| ~SPC m M-RET~   | Insert regular match branch                                     |
+| ~SPC m M-S-RET~ | Insert =match goal with= branch                                 |
+| ~SPC m i e~     | Insert =End <section-name>=                                     |
+| ~SPC m i l~     | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) |
+| ~SPC m i m~     | Insert =match= on a type                                        |
 
 Note the last two are regular =company-coq= bindings, left alone since they are
 most useful in insert mode. The full =company-coq= tutorial showcasing all
@@ -96,7 +94,7 @@ company-coq-tutorial=.
 ** There are empty square boxes in place of math operators
 Math symbols present in your buffer (e.g. forall exists) will attempt to be
 prettified, if you are seeing empty square boxes this means an appropriate math
-symbol cannot be found in your font. You can either install a appropriate math
+symbol cannot be found in your *font*. You can either install a appropriate math
 font, or disable the feature by adding the following snippet to the your
 =dotspacemacs/user-config=.
 

diff --git a/layers/+lang/coq/config.el b/layers/+lang/coq/config.el
@@ -0,0 +1,14 @@
+;;; packages.el --- Coq Layer configuration File for Spacemacs
+;;
+;; Copyright (c) 2012-2017 Sylvain Benner & Contributors
+;;
+;; Author: Sylvain Benner <sylvain.benner@gmail.com>
+;; URL: https://github.com/syl20bnr/spacemacs
+;;
+;; This file is not part of GNU Emacs.
+;;
+;;; License: GPLv3
+
+;; variables
+
+(spacemacs|define-jump-handlers coq-mode)
diff --git a/layers/+lang/coq/packages.el b/layers/+lang/coq/packages.el
@@ -25,7 +25,11 @@
 (defun coq/init-company-coq ()
   (use-package company-coq
     :defer t
-    :init (add-hook 'coq-mode-hook #'company-coq-mode)
+    :init
+    (progn
+      (add-hook 'coq-mode-hook #'company-coq-mode)
+      (add-to-list 'spacemacs-jump-handlers-coq-mode
+                   'company-coq-jump-to-definition))
     :config
     (progn
       (spacemacs/declare-prefix-for-mode
@@ -34,8 +38,7 @@
       (spacemacs/set-leader-keys-for-major-mode 'coq-mode
         "il" 'company-coq-lemma-from-goal
         "im" 'company-coq-insert-match-construct
-        "ao" 'company-coq-occur
-        "gd" 'company-coq-jump-to-definition))))
+        "ao" 'company-coq-occur))))
 
 (defun coq/init-proof-general ()
   (use-package proof-site
@@ -78,29 +81,29 @@
         "[" 'proof-undo-last-successful-command
         "." 'proof-goto-point
         ;; Layout
-        "ll" 'proof-layout-windows
         "lc" 'pg-response-clear-displays
+        "ll" 'proof-layout-windows
         "lp" 'proof-prf
         ;; Prover Interaction
-        "px" 'proof-shell-exit
-        "pc" 'proof-interrupt-process
+        "pi" 'proof-interrupt-process
+        "pp" 'proof-process-buffer
+        "pq" 'proof-shell-exit
         "pr" 'proof-retract-buffer
-        "pb" 'proof-process-buffer
         ;; Prover queries ('ask prover')
-        "af" 'proof-find-theorems
-        "ap" 'coq-Print
-        "ac" 'coq-Check
+        "aa" 'coq-Print
+        "aA" 'coq-Print-with-all
         "ab" 'coq-About
-        "aip" 'coq-Print-with-implicits
-        "aic" 'coq-Check-show-implicits
+        "aB" 'coq-About-with-all
+        "ac" 'coq-Check
+        "aC" 'coq-Check-show-all
+        "af" 'proof-find-theorems
         "aib" 'coq-About-with-implicits
-        "anp" 'coq-Print-with-all
-        "anc" 'coq-Check-show-all
-        "anb" 'coq-About-with-all
+        "aic" 'coq-Check-show-implicits
+        "aii" 'coq-Print-with-implicits
         ;; Moving the point (goto)
-        "g." 'proof-goto-end-of-locked
-        "ga" 'proof-goto-command-start
         "ge" 'proof-goto-command-end
+        "gl" 'proof-goto-end-of-locked
+        "gs" 'proof-goto-command-start
         ;; Insertions
         "ie" 'coq-end-Section))))