From 7e7577e82bab1e699133d1173173ab8e0cf4d2e4 Mon Sep 17 00:00:00 2001 From: Richard Copley Date: Sat, 2 Mar 2024 01:01:40 +0000 Subject: [PATCH] fix: magit-section usage Use named sections so magit-section can track which sections are expanded. Don't use sections for individual diagnostics, since they can't be tracked. Capture data in lexicals for deferred rendering by `magit-insert-section-body'. Use `with-current-buffer` (delete `lean4-with-info-output-to-buffer`). Make the diagnostic `line:col` headers into text buttons. --- lean4-info.el | 111 +++++++++++++++++++++++++++++--------------------- 1 file changed, 65 insertions(+), 46 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 1b6ccd6..5d6817f 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -54,16 +54,6 @@ (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function)) -(defmacro lean4-with-info-output-to-buffer (buffer &rest body) - "Execute BODY redirecting `print' output to BUFFER." - `(let ((buf (get-buffer ,buffer))) - (with-current-buffer buf - (setq buffer-read-only nil) - (erase-buffer) - (let ((standard-output buf)) - ,@body) - (setq buffer-read-only t)))) - (defun lean4-ensure-info-buffer (buffer) "Create BUFFER if it does not exist. Also choose settings used for the *Lean Goal* buffer." @@ -106,22 +96,57 @@ The buffer is supposed to be the *Lean Goal* buffer." (lsp-defun lean4-diagnostic-full-end-line ((&lean:Diagnostic :full-range (&Range :end (&Position :line)))) line) -(defun lean4-mk-message-section (caption errors) - "Add a section with caption CAPTION and contents ERRORS." - (when errors - (magit-insert-section (magit-section) +(defun lean4-info--error-button-action (data) + (let ((buffer (nth 0 data)) + (line (nth 1 data)) + (column (nth 2 data))) + (when (buffer-live-p buffer) + (pop-to-buffer buffer) + (goto-char (point-min)) + (forward-line (1- line)) + (forward-char column)))) + +(defun lean4-info--insert-highlight-inaccessible-names (&rest text) + (let ((begin (point))) + (apply #'insert text) + (when lean4-highlight-inaccessible-names + (let ((end (point-marker))) + (goto-char begin) + (while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" end t) + (replace-match + (propertize (concat (match-string-no-properties 1) + (match-string-no-properties 2)) + 'font-lock-face 'font-lock-comment-face) + 'fixedcase 'literal)) + (goto-char end))))) + +(defun lean4--insert-goal-text (text delimiter) + (lean4-info--insert-highlight-inaccessible-names + (lsp--fontlock-with-mode text 'lean4-info-mode) + delimiter)) + +(defun lean4-info--mk-message-section (value caption messages buffer) + "Add a section with id VALUE, caption CAPTION and contents ERRORS." + (when-let (msgs messages) ;; captured for deferred rendering + (magit-insert-section (magit-section value) (magit-insert-heading caption) (magit-insert-section-body - (dolist (e errors) + (dolist (e msgs) (-let (((&Diagnostic :message :range (&Range :start (&Position :line :character))) e)) - (magit-insert-section (magit-section) - (magit-insert-heading (format "%d:%d: " (1+ (lsp-translate-line line)) (lsp-translate-column character))) - (magit-insert-section-body - (insert message "\n"))))))))) + (let ((ln (1+ (lsp-translate-line line))) + (col (lsp-translate-column character))) + (insert-text-button (format "%d:%d:" ln col) + 'action #'lean4-info--error-button-action + 'button-data (list buffer ln col) + 'face 'magit-section-heading + 'help-echo "mouse-2: visit this file, line and column")) + (lean4-info--insert-highlight-inaccessible-names "\n" message "\n"))))))) (defun lean4-info-buffer-redisplay () (when (lean4-info-buffer-active lean4-info-buffer-name) (-let* ((deactivate-mark) ; keep transient mark + (inhibit-read-only t) + (buffer (current-buffer)) (line (lsp--cur-line)) (errors (lsp--get-buffer-diagnostics)) (errors (-sort (-on #'< #'lean4-diagnostic-full-end-line) errors)) @@ -129,33 +154,27 @@ The buffer is supposed to be the *Lean Goal* buffer." (--split-with (< (lean4-diagnostic-full-end-line it) line) errors)) ((errors-here errors-below) (--split-with (<= (lean4-diagnostic-full-start-line it) line) errors))) - (lean4-with-info-output-to-buffer - lean4-info-buffer-name - (when lean4-goals - (magit-insert-section (magit-section) - (magit-insert-heading "Goals:") - (magit-insert-section-body - (if (> (length lean4-goals) 0) - (seq-doseq (g lean4-goals) - (magit-insert-section (magit-section) - (insert (lsp--fontlock-with-mode g 'lean4-info-mode) "\n\n"))) - (insert "goals accomplished\n\n"))))) - (when lean4-term-goal - (magit-insert-section (magit-section) - (magit-insert-heading "Expected type:") - (magit-insert-section-body - (insert (lsp--fontlock-with-mode lean4-term-goal 'lean4-info-mode) "\n")))) - (lean4-mk-message-section "Messages here:" errors-here) - (lean4-mk-message-section "Messages below:" errors-below) - (lean4-mk-message-section "Messages above:" errors-above) - (when lean4-highlight-inaccessible-names - (goto-char 0) - (while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" nil t) - (replace-match - (propertize (concat (match-string-no-properties 1) (match-string-no-properties 2)) - 'font-lock-face 'font-lock-comment-face) - 'fixedcase 'literal))))))) - + (with-current-buffer lean4-info-buffer-name + (progn + (erase-buffer) + (magit-insert-section (magit-section 'root) + (when-let ((goals lean4-goals)) ;; capture for deferred rendering + (magit-insert-section (magit-section 'goals) + (magit-insert-heading "Goals:") + (magit-insert-section-body + (if (> (length goals) 0) + (seq-doseq (g goals) + (magit-insert-section (magit-section) + (lean4--insert-goal-text g "\n\n"))) + (insert "goals accomplished\n\n"))))) + (when-let ((term-goal lean4-term-goal)) ;; capture for deferred rendering + (magit-insert-section (magit-section 'term-goal) + (magit-insert-heading "Expected type:") + (magit-insert-section-body + (lean4--insert-goal-text term-goal "\n")))) + (lean4-info--mk-message-section 'errors-here "Messages here:" errors-here buffer) + (lean4-info--mk-message-section 'errors-below "Messages below:" errors-below buffer) + (lean4-info--mk-message-section 'errors-above "Messages above:" errors-above buffer))))))) ;; Debouncing ;; ~~~~~~~~~~~