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

fix(emacs): clear error messages in next-error-mode

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-26 16:09:42 -04:00 • committed by Leonardo de Moura
parent d071594b8e
commit 7cff9c4498
1 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/emacs/lean-flycheck.el
View file

@ -119,14 +119,13 @@
(e (get-char-property pos 'flycheck-error)))
(setq errors (list e))))
(when errors
(with-output-to-lean-info
(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)))))))))
(with-output-to-lean-info
(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))))))))
(define-minor-mode lean-next-error-mode
"Toggle lean-next-error-mode on and off.