diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el index 18e26ff39..a4a6ab8a7 100644 --- a/src/emacs/lean-flycheck.el +++ b/src/emacs/lean-flycheck.el @@ -68,4 +68,33 @@ (add-hook 'lean-mode-hook '(lambda () (when lean-flycheck-use (lean-flycheck-turn-on)))) +(defun lean-flycheck-try-parse-error-with-pattern (err pattern) + "Try to parse a single ERR with a PATTERN. + +Return the parsed error if PATTERN matched ERR, or nil +otherwise." + (let ((regexp (car pattern)) + (level (cdr pattern))) + (when (string-match regexp err) + (let ((filename (match-string 1 err)) + (line (match-string 2 err)) + (column (match-string 3 err)) + (message (match-string 4 err))) + (flycheck-error-new + :filename (unless (string-empty-p filename) filename) + :line (flycheck-string-to-number-safe line) + :column (let ((col (flycheck-string-to-number-safe column))) + (if (= col 0) 1 col)) + :message (unless (string-empty-p message) message) + :level level))))) + +(eval-after-load "flycheck.el" + '(defadvice flycheck-try-parse-error-with-pattern + (after lean-flycheck-try-parse-error-with-pattern activate) + "Add 1 to error-column." + (let* ((err ad-return-value) + (col (flycheck-error-column err))) + (when (and (string= major-mode "lean-mode") col) + (setf (flycheck-error-column ad-return-value) (1+ col)))))) + (provide 'lean-flycheck)