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

feat: lean4-mode: show "goals accomplished"

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-26 12:59:38 +01:00
parent f8adb449fe
commit 9e3b8caa4b
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
lean4-mode/lean4-info.el
View file

@ -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