max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: lean4-mode: lean4-refresh-file-dependencies (C-c C-d)

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-25 18:18:17 +01:00
parent 1945ebd275
commit 1cfc4cecc1
3 changed files with 27 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
lean4-mode/README.md
View file

@ -45,17 +45,17 @@ Set these with e.g. `M-x customize-variable`.
Key Bindings and Commands
=========================
| Key | Function |
|--------------------|---------------------------------------------------------------------------------|
| <kbd>C-c C-k</kbd> | shows the keystroke needed to input the symbol under the cursor |
| <kbd>C-c C-x</kbd> | execute lean in stand-alone mode (`lean-std-exe`) |
| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
| <kbd>C-c ! n</kbd> | flycheck: go to next error |
| <kbd>C-c ! p</kbd> | flycheck: go to previous error |
| <kbd>C-c ! l</kbd> | flycheck: show list of errors |
| Key | Function |
|--------------------|--------------------------------------------------------------------------|
| <kbd>C-c C-k</kbd> | show the keystroke needed to input the symbol under the cursor |
| <kbd>C-c C-d</kbd> | recompile & reload imports (`lean-refresh-file-dependencies`) |
| <kbd>C-c C-x</kbd> | execute Lean in stand-alone mode (`lean-std-exe`) |
| <kbd>C-c C-n</kbd> | toggle showing next error in dedicated buffer (`lean-toggle-next-error`) |
| <kbd>C-c ! n</kbd> | flycheck: go to next error |
| <kbd>C-c ! p</kbd> | flycheck: go to previous error |
| <kbd>C-c ! l</kbd> | flycheck: show list of errors |
For `lsp-mode` bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently).
Of note is `s-l s r` for restarting the server, which can be used to make Lean reload changed imports.
In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the
number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu.

15
lean4-mode/lean4-mode.el
View file

@ -75,6 +75,20 @@
(interactive)
(lean4-execute))
(defun lean4-refresh-file-dependencies ()
"Restart the server subprocess for the current file, recompiling & reloading all imports"
(interactive)
(lsp-notify
"textDocument/didClose"
`(:textDocument ,(lsp--text-document-identifier)))
(lsp-notify
"textDocument/didOpen"
(list :textDocument
(list :uri (lsp--buffer-uri)
:languageId (lsp-buffer-language)
:version lsp--cur-version
:text (lsp--buffer-content)))))
(defun lean4-check-expansion ()
(interactive)
(save-excursion
@ -104,6 +118,7 @@
(local-set-key lean4-keybinding-leanpkg-configure #'lean4-leanpkg-configure)
(local-set-key lean4-keybinding-leanpkg-build #'lean4-leanpkg-build)
(local-set-key lean4-keybinding-leanpkg-test #'lean4-leanpkg-test)
(local-set-key lean4-keybinding-refresh-file-dependencies #'lean4-refresh-file-dependencies)
;; This only works as a mouse binding due to the event, so it is not abstracted
;; to avoid user confusion.
(local-set-key (kbd "<mouse-3>") #'lean4-right-click-show-menu)

3
lean4-mode/lean4-settings.el
View file

@ -129,4 +129,7 @@ false (nil)."
(defcustom lean4-keybinding-leanpkg-test (kbd "C-c C-p C-t")
"Lean Keybinding for lean4-leanpkg-test"
:group 'lean4-keybinding :type 'key-sequence)
(defcustom lean4-keybinding-refresh-file-dependencies (kbd "C-c C-d")
"Lean Keybinding for lean4-refresh-file-dependencies"
:group 'lean4-keybinding :type 'key-sequence)
(provide 'lean4-settings)