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

fix(emacs/lean-flycheck): only update next-error-mode for current buffer

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-12 21:46:08 +01:00 • committed by Leonardo de Moura
parent 51924eb726
commit ab539971a6
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -133,7 +133,9 @@
(defconst lean-next-error-buffer-name "*Lean Next Error*")
(defun lean-next-error-copy ()
(when (and (equal major-mode 'lean-mode))
(when (and (equal major-mode 'lean-mode)
; check whether current window of current buffer is selected (i.e., in focus)
(eq (current-buffer) (window-buffer)))
(let* ((errors (sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position))
#'flycheck-error-<)))