From 66969328a23c0d773bb41df20ba092f5750651de Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 29 Apr 2016 17:14:09 -0400 Subject: [PATCH] feat(src/emacs/README.md): add more information about key bindings and commands --- src/emacs/README.md | 37 +++++++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/src/emacs/README.md b/src/emacs/README.md index ddbfdf70a7..40e69a4e67 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -151,19 +151,32 @@ you type, an asterisk should briefly appear after ``FlyC``, indicating that your file is being checked. -Key Bindings -============ +Key Bindings and Commands +========================= -|Key | Function | -|-------------------|-----------------------------------| -|C-c C-x | lean-std-exe | -|C-c C-l | lean-std-exe | -|C-c C-t | lean-eldoc-documentation-function | -|C-c C-f | lean-fill-placeholder | -|M-. | lean-find-tag | -|TAB | lean-tab-indent-or-complete | -|C-c C-o | lean-set-option | -|C-c C-e | lean-eval-cmd | +|Key | Function | +|-------------------|-------------------------------------------------------------------------------| +|M-. | jump to definition in source file (lean-find-tag) | +|TAB | tab complete identifier, option, filename, etc. (lean-tab-indent-or-complete) | +|C-c C-k | shows the keystroke needed to input the symbol under the cursor | +|C-c C-g | show goal in tactic proof (lean-show-goal-at-pos) | +|C-c C-p | print information about identifier (lean-show-id-keyword-info) | +|C-c C-t | show type (lean-show-type) | +|C-c C-f | replace underscore by inferred value (lean-fill-placeholder) | +|C-c C-x | execute lean in stand-alone mode (lean-std-exe) | +|C-c C-l | execute lean in stand-alone mode (lean-std-exe) | +|C-c C-o | set option (lean-set-option) | +|C-c C-r | restart lean process (lean-server-reset-process) | +|C-c C-e | lean-eval-cmd | +|C-c ! n | flycheck: go to next error | +|C-c ! p | flycheck: go to previous error | +|C-c ! l | flycheck: show list of errors | + +The Flycheck annotation `FlyC:n/n` indicates the number of errors / responses from Lean. An asterisk +`*FlyC:n/n` indicates that checking is in progress. Clicking on `FlyC` opens the Flycheck menu. + +To profile Lean performace on the file in the buffer, enter M-x lean-execute or choose +`Lean execute` from the Lean menu, and add the option `--profile`. Known Issues and Possible Solutions