From 03af37c29de81503e62249da9140fbd9955c9375 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Mar 2021 21:20:07 +0100 Subject: [PATCH] doc: lean4-mode: update keybindings --- lean4-mode/README.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/lean4-mode/README.md b/lean4-mode/README.md index 00b8f552dd..95251d5413 100644 --- a/lean4-mode/README.md +++ b/lean4-mode/README.md @@ -45,15 +45,14 @@ Set these with e.g. `M-x customize-variable`. Key Bindings and Commands ========================= -| Key | Function | -|--------------------|--------------------------------------------------------------------------| -| C-c C-k | show the keystroke needed to input the symbol under the cursor | -| C-c C-d | recompile & reload imports (`lean-refresh-file-dependencies`) | -| C-c C-x | execute Lean in stand-alone mode (`lean-std-exe`) | -| C-c C-n | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) | -| C-c ! n | flycheck: go to next error | -| C-c ! p | flycheck: go to previous error | -| C-c ! l | flycheck: show list of errors | +| Key | Function | +|--------------------|---------------------------------------------------------------------------------| +| C-c C-k | show the keystroke needed to input the symbol under the cursor | +| C-c C-d | recompile & reload imports (`lean4-refresh-file-dependencies`) | +| C-c C-x | execute Lean in stand-alone mode (`lean4-std-exe`) | +| C-c C-i | toggle info view showing goals and errors at point (`lean4-toggle-info-buffer`) | +| C-c ! n | flycheck: go to next error | +| C-c ! p | flycheck: go to previous error | For `lsp-mode` bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently).