diff --git a/lean4-mode/lean4-info.el b/lean4-mode/lean4-info.el index 80de0d420c..29a321f892 100644 --- a/lean4-mode/lean4-info.el +++ b/lean4-mode/lean4-info.el @@ -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) "")) + (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) diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el index b9d2981e4e..8dcceb7aee 100644 --- a/lean4-mode/lean4-mode.el +++ b/lean4-mode/lean4-mode.el @@ -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 diff --git a/lean4-mode/lean4-settings.el b/lean4-mode/lean4-settings.el index bc3e847c50..03e71f4c89 100644 --- a/lean4-mode/lean4-settings.el +++ b/lean4-mode/lean4-settings.el @@ -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"