From 9e3b8caa4b77f6ef1f227d12094bb7f97fdfc450 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 26 Mar 2021 12:59:38 +0100 Subject: [PATCH] feat: lean4-mode: show "goals accomplished" --- lean4-mode/lean4-info.el | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/lean4-mode/lean4-info.el b/lean4-mode/lean4-info.el index 038fae6460..f5f00b26c3 100644 --- a/lean4-mode/lean4-info.el +++ b/lean4-mode/lean4-info.el @@ -87,9 +87,11 @@ (magit-insert-section (magit-section) (magit-insert-heading "Goals:") (magit-insert-section-body - (dolist (g lean4-goals) - (magit-insert-section (magit-section) - (insert g "\n\n")))))) + (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 selected-errors (magit-insert-section (magit-section) (magit-insert-heading "Messages:") @@ -117,7 +119,7 @@ "$/lean/plainGoal" (lsp--text-document-position-params) (-lambda ((goal &as &lean:PlainGoal? :goals)) - (setq lean4-goals (--map (lsp--fontlock-with-mode it 'lean4-info-mode) goals)) + (setq lean4-goals goals) (lean4-info-buffer-redisplay)) :error-handler #'ignore :mode 'tick