feat: lean4-mode: combine goal and next-error views into info view (C-c C-i)
This commit is contained in:
Sebastian Ullrich
parent
d2f9e43ca0
commit
14e11f99e6
3 changed files with 44 additions and 57 deletions
|
|
@ -62,41 +62,12 @@
|
|||
(lsp-interface
|
||||
(lean:PlainGoal (:rendered) nil))
|
||||
|
||||
(defconst lean4-show-goal-buffer-name "*Lean Goal*")
|
||||
(defconst lean4-info-buffer-name "*Lean Goal*")
|
||||
|
||||
(defun lean4-show-goal--handler ()
|
||||
(let ((deactivate-mark)) ; keep transient mark
|
||||
(when (lean4-info-buffer-active lean4-show-goal-buffer-name)
|
||||
(lsp-request-async
|
||||
"$/lean/plainGoal"
|
||||
(lsp--text-document-position-params)
|
||||
(-lambda ((goal &as &lean:PlainGoal? :rendered))
|
||||
(when goal
|
||||
(let ((rerendered (lsp--render-string rendered "markdown")))
|
||||
(lean4-with-info-output-to-buffer
|
||||
lean4-show-goal-buffer-name
|
||||
(insert rerendered)
|
||||
(when lean4-highlight-inaccessible-names
|
||||
(goto-char 0)
|
||||
(while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" nil t)
|
||||
(replace-match
|
||||
(propertize (s-concat (match-string-no-properties 1) (match-string-no-properties 2))
|
||||
'font-lock-face 'font-lock-comment-face)
|
||||
'fixedcase 'literal)))))))
|
||||
:error-handler #'ignore
|
||||
:mode 'tick
|
||||
:cancel-token :plain-goal))))
|
||||
(defvar lean4-goal "")
|
||||
|
||||
(defun lean4-toggle-show-goal ()
|
||||
"Show goal at the current point."
|
||||
(interactive)
|
||||
(lean4-toggle-info-buffer lean4-show-goal-buffer-name)
|
||||
(lean4-show-goal--handler))
|
||||
|
||||
(defconst lean4-next-error-buffer-name "*Lean Next Error*")
|
||||
|
||||
(defun lean4-next-error--handler ()
|
||||
(when (lean4-info-buffer-active lean4-next-error-buffer-name)
|
||||
(defun lean4-info-buffer-redisplay ()
|
||||
(when (lean4-info-buffer-active lean4-info-buffer-name)
|
||||
(let ((deactivate-mark) ; keep transient mark
|
||||
(errors (or
|
||||
;; prefer error of current position, if any
|
||||
|
|
@ -107,17 +78,44 @@
|
|||
;; fall back to next error position
|
||||
(-if-let* ((pos (flycheck-next-error-pos 1)))
|
||||
(flycheck-overlay-errors-at pos)))))
|
||||
(lean4-with-info-output-to-buffer lean4-next-error-buffer-name
|
||||
(lean4-with-info-output-to-buffer
|
||||
lean4-info-buffer-name
|
||||
(insert (or (s-trim lean4-goal) "<no goals>"))
|
||||
(insert "\n---\n")
|
||||
(dolist (e errors)
|
||||
(princ (format "%d:%d: " (flycheck-error-line e) (flycheck-error-column e)))
|
||||
(princ (flycheck-error-message e))
|
||||
(princ "\n\n"))
|
||||
(when flycheck-current-errors
|
||||
(princ (format "(%d more messages above...)" (length flycheck-current-errors))))))))
|
||||
(princ (format "(%d more messages above...)" (length flycheck-current-errors))))
|
||||
(when lean4-highlight-inaccessible-names
|
||||
(goto-char 0)
|
||||
(while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" nil t)
|
||||
(replace-match
|
||||
(propertize (s-concat (match-string-no-properties 1) (match-string-no-properties 2))
|
||||
'font-lock-face 'font-lock-comment-face)
|
||||
'fixedcase 'literal)))))))
|
||||
|
||||
(defun lean4-toggle-next-error ()
|
||||
(defun lean4-info-buffer-refresh ()
|
||||
(when (lean4-info-buffer-active lean4-info-buffer-name)
|
||||
(lsp-request-async
|
||||
"$/lean/plainGoal"
|
||||
(lsp--text-document-position-params)
|
||||
(-lambda ((goal &as &lean:PlainGoal? :rendered))
|
||||
(let ((rerendered (lsp--render-string rendered "markdown")))
|
||||
(setq lean4-goal rerendered)
|
||||
(lean4-info-buffer-redisplay)))
|
||||
:error-handler #'ignore
|
||||
:mode 'tick
|
||||
:cancel-token :plain-goal)
|
||||
;; may lead to flickering
|
||||
;(lean4-info-buffer-redisplay)
|
||||
))
|
||||
|
||||
(defun lean4-toggle-info ()
|
||||
"Show infos at the current point."
|
||||
(interactive)
|
||||
(lean4-toggle-info-buffer lean4-next-error-buffer-name)
|
||||
(lean4-next-error--handler))
|
||||
(lean4-toggle-info-buffer lean4-info-buffer-name)
|
||||
(lean4-info-buffer-refresh))
|
||||
|
||||
(provide 'lean4-info)
|
||||
|
|
|
|||
|
|
@ -97,8 +97,7 @@
|
|||
(local-set-key lean4-keybinding-find-definition #'lean4-find-definition)
|
||||
(local-set-key lean4-keybinding-tab-indent #'lean4-tab-indent)
|
||||
(local-set-key lean4-keybinding-hole #'lean4-hole)
|
||||
(local-set-key lean4-keybinding-lean4-toggle-show-goal #'lean4-toggle-show-goal)
|
||||
(local-set-key lean4-keybinding-lean4-toggle-next-error #'lean4-toggle-next-error)
|
||||
(local-set-key lean4-keybinding-lean4-toggle-info #'lean4-toggle-info)
|
||||
(local-set-key lean4-keybinding-lean4-message-boxes-toggle #'lean4-message-boxes-toggle)
|
||||
(local-set-key lean4-keybinding-leanpkg-configure #'lean4-leanpkg-configure)
|
||||
(local-set-key lean4-keybinding-leanpkg-build #'lean4-leanpkg-build)
|
||||
|
|
@ -126,8 +125,7 @@
|
|||
;; ["Create a new project" (call-interactively 'lean4-project-create) (not (lean4-project-inside-p))]
|
||||
"-----------------"
|
||||
["Show type info" lean4-show-type (and lean4-eldoc-use eldoc-mode)]
|
||||
["Toggle goal display" lean4-toggle-show-goal t]
|
||||
["Toggle next error display" lean4-toggle-next-error t]
|
||||
["Toggle info display" lean4-toggle-info t]
|
||||
["Toggle message boxes" lean4-message-boxes-toggle t]
|
||||
["Highlight pending tasks" lean4-server-toggle-show-pending-tasks
|
||||
:active t :style toggle :selected lean4-server-show-pending-tasks]
|
||||
|
|
@ -154,10 +152,8 @@
|
|||
;; Handle events that may start automatic syntax checks
|
||||
(before-save-hook . lean4-whitespace-cleanup)
|
||||
;; info windows
|
||||
(post-command-hook . lean4-show-goal--handler)
|
||||
(post-command-hook . lean4-next-error--handler)
|
||||
;; (flycheck-after-syntax-check-hook . lean4-show-goal--handler)
|
||||
(flycheck-after-syntax-check-hook . lean4-next-error--handler)
|
||||
(post-command-hook . lean4-info-buffer-refresh)
|
||||
(flycheck-after-syntax-check-hook . lean4-info-buffer-refresh)
|
||||
)
|
||||
"Hooks which lean4-mode needs to hook in.
|
||||
|
||||
|
|
@ -171,11 +167,7 @@ enabled and disabled respectively.")
|
|||
;;(setq lean4-right-click-item-functions '(lean4-info-right-click-find-definition
|
||||
;; lean4-hole-right-click))
|
||||
;; Flycheck
|
||||
(setq-local flycheck-disabled-checkers '())
|
||||
;; info buffers
|
||||
(lean4-ensure-info-buffer lean4-next-error-buffer-name)
|
||||
;(lean4-ensure-info-buffer lean4-show-goal-buffer-name)
|
||||
)
|
||||
(setq-local flycheck-disabled-checkers '()))
|
||||
|
||||
;; Automode List
|
||||
;;;###autoload
|
||||
|
|
|
|||
|
|
@ -57,7 +57,7 @@ written."
|
|||
:type 'boolean)
|
||||
|
||||
(defcustom lean4-highlight-inaccessible-names t
|
||||
"Set this variable to `t` to highlight inaccessible names in the goal display
|
||||
"Set this variable to `t` to highlight inaccessible names in the info display
|
||||
using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
|
||||
:group 'lean
|
||||
:type 'boolean)
|
||||
|
|
@ -89,11 +89,8 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
|
|||
(defcustom lean4-keybinding-hole (kbd "C-c SPC")
|
||||
"Lean Keybinding for hole manipulation"
|
||||
:group 'lean4-keybinding :type 'key-sequence)
|
||||
(defcustom lean4-keybinding-lean4-toggle-show-goal (kbd "C-c C-g")
|
||||
"Lean Keybinding for show-goal-at-pos"
|
||||
:group 'lean4-keybinding :type 'key-sequence)
|
||||
(defcustom lean4-keybinding-lean4-toggle-next-error (kbd "C-c C-n")
|
||||
"Lean Keybinding for lean4-toggle-next-error"
|
||||
(defcustom lean4-keybinding-lean4-toggle-info (kbd "C-c C-i")
|
||||
"Lean Keybinding for lean4-toggle-info"
|
||||
:group 'lean4-keybinding :type 'key-sequence)
|
||||
(defcustom lean4-keybinding-lean4-message-boxes-toggle (kbd "C-c C-b")
|
||||
"Lean Keybinding for lean4-message-boxes-toggle"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue