michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-type): output INFO to *lean-info* buffer in addition to minibuffer

Browse source 
Close #260
This commit is contained in:
Soonho Kong 2014-10-28 14:06:03 -07:00
parent 0d8658d762
commit b0e249ce63
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/emacs/lean-type.el
View file

@ -40,7 +40,11 @@
(when add-to-kill-ring (when add-to-kill-ring
(kill-new (kill-new
(substring-no-properties info-string))) (substring-no-properties info-string)))
(message "%s" info-string)))) (when (or lean-show-proofstate-in-minibuffer
(not (lean-info-record-proofstate info-record)))
(message "%s" info-string))
(lean-output-to-buffer "*lean-info*" "--------------------------\n" nil)
(lean-output-to-buffer "*lean-info*" "%s\n" (list info-string)))))
(defun lean-eldoc-documentation-function (&optional add-to-kill-ring) (defun lean-eldoc-documentation-function (&optional add-to-kill-ring)
"Show information of lean expression at point if any" "Show information of lean expression at point if any"