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

feat(emacs/lean-flycheck): Next Error: show all errors at current or next position

Browse source
This commit is contained in:
Sebastian Ullrich 2017-02-01 15:39:00 +01:00 • committed by Leonardo de Moura
parent c3a655fdae
commit 1bcdbf38bd
1 changed files with 9 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -117,19 +117,15 @@
(defun lean-next-error--handler ()
(when (lean-info-buffer-active lean-next-error-buffer-name)
(let* ((errors (sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position))
#'flycheck-error-<)))
;; prefer error of current position, if any
(-if-let (e (get-char-property (point) 'flycheck-error))
(setq errors (list e)))
;; fall back to next error
(if (null errors)
(-if-let* ((pos (flycheck-next-error-pos 1))
(e (get-char-property pos 'flycheck-error)))
(setq errors (list e))))
(let ((errors (or
;; prefer error of current position, if any
(flycheck-overlay-errors-at (point))
;; try errors in current line next
(sort (flycheck-overlay-errors-in (line-beginning-position) (line-end-position))
#'flycheck-error-<)
;; fall back to next error position
(-if-let* ((pos (flycheck-next-error-pos 1)))
(flycheck-overlay-errors-at pos)))))
(lean-with-info-output-to-buffer lean-next-error-buffer-name
(dolist (e errors)
(princ (format "%d:%d: " (flycheck-error-line e) (flycheck-error-column e)))