126 lines
4.5 KiB
EmacsLisp
126 lines
4.5 KiB
EmacsLisp
;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
|
;; Released under Apache 2.0 license as described in the file LICENSE.
|
|
;;
|
|
;; Author: Soonho Kong
|
|
;;
|
|
|
|
(require 'lean-settings)
|
|
(require 'lean-option)
|
|
|
|
(defun lean-toggle-flycheck-mode ()
|
|
"Toggle flycheck-mode"
|
|
(interactive)
|
|
(cond
|
|
(flycheck-mode (flycheck-mode -1))
|
|
(t (flycheck-mode 1))))
|
|
|
|
(defun lean-flycheck-command ()
|
|
"Concat lean-flychecker-checker-name with options"
|
|
(let ((command
|
|
(cl-concatenate 'list
|
|
`(,(lean-get-executable lean-flycheck-checker-name))
|
|
lean-flycheck-checker-options
|
|
'("--cache")
|
|
'(source-original)
|
|
'((eval (lean-option-string t)))
|
|
'("--")
|
|
'(source-inplace))))
|
|
(when (string= system-type "windows-nt")
|
|
(setq command (cons "python" command)))
|
|
command))
|
|
|
|
(defun lean-flycheck-init ()
|
|
"Initialize lean-flychek checker"
|
|
(eval
|
|
`(flycheck-define-checker lean-checker
|
|
"A Lean syntax checker."
|
|
:command ,(lean-flycheck-command)
|
|
:error-patterns
|
|
((error line-start "FLYCHECK_BEGIN ERROR" (? "\r") "\n"
|
|
(file-name) ":" line ":" (? column ":") " error: "
|
|
(minimal-match
|
|
(message (one-or-more (zero-or-more not-newline) (? "\r") "\n")))
|
|
"FLYCHECK_END" (? "\r") line-end)
|
|
(warning line-start "FLYCHECK_BEGIN INFORMATION" (? "\r") "\n"
|
|
(file-name) ":" line ":" (? column ":") " information: "
|
|
(minimal-match
|
|
(message (one-or-more (zero-or-more not-newline) (? "\r") "\n")))
|
|
"FLYCHECK_END" (? "\r") line-end)
|
|
;; (warning line-start "FLYCHECK_BEGIN WARNING" (? "\r") "\n"
|
|
;; (file-name) ":" line ":" (? column ":") " warning: "
|
|
;; (minimal-match
|
|
;; (message (one-or-more (zero-or-more not-newline) (? "\r") "\n")))
|
|
;; "FLYCHECK_END" (? "\r") line-end)
|
|
)
|
|
:modes (lean-mode)))
|
|
(add-to-list 'flycheck-checkers 'lean-checker))
|
|
|
|
(defun lean-flycheck-turn-on ()
|
|
(interactive)
|
|
(unless lean-flycheck-use
|
|
(when (interactive-p)
|
|
(message "use flycheck in lean-mode"))
|
|
(setq lean-flycheck-use t))
|
|
(flycheck-mode t))
|
|
|
|
(defun lean-flycheck-turn-off ()
|
|
(interactive)
|
|
(when lean-flycheck-use
|
|
(when (interactive-p)
|
|
(message "no flycheck in lean-mode")))
|
|
(flycheck-mode 0)
|
|
(setq lean-flycheck-use nil))
|
|
|
|
(defun lean-flycheck-toggle-use ()
|
|
(interactive)
|
|
(if lean-flycheck-use
|
|
(lean-flycheck-turn-off)
|
|
(lean-flycheck-turn-on)))
|
|
|
|
(eval-after-load "flycheck"
|
|
'(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 (and err (flycheck-error-column err))))
|
|
(when (and (string= major-mode "lean-mode") col)
|
|
(setf (flycheck-error-column ad-return-value) (1+ col))))))
|
|
|
|
(defun lean-flycheck-delete-temporaries ()
|
|
"Delete temporaries files generated by flycheck."
|
|
(when (eq major-mode 'lean-mode)
|
|
(let* ((filename (buffer-file-name))
|
|
(tempname (format "%s_%s"
|
|
flycheck-temp-prefix
|
|
(file-name-nondirectory filename)))
|
|
(tempbase (file-name-base tempname))
|
|
(tempfile (expand-file-name tempbase
|
|
(file-name-directory filename)))
|
|
(exts '(".ilean" ".d" ".olean"))
|
|
(tempfiles (--map (concat tempfile it) exts)))
|
|
(mapc #'flycheck-safe-delete tempfiles))))
|
|
|
|
|
|
(defun lean-flycheck-error-list-buffer-width ()
|
|
"Return the width of flycheck-error list buffer"
|
|
(interactive)
|
|
(let* ((flycheck-error-window (get-buffer-window "*Flycheck errors*" t))
|
|
(window (selected-window))
|
|
(body-width (window-body-width window)))
|
|
(cond
|
|
;; If "*Flycheck errors" buffer is available, use its width
|
|
(flycheck-error-window
|
|
(window-body-width flycheck-error-window))
|
|
;; If lean-flycheck-msg-width is set, use it
|
|
(lean-flycheck-msg-width
|
|
lean-flycheck-msg-width)
|
|
;; Can we split vertically?
|
|
((window-splittable-p window nil)
|
|
body-width)
|
|
;; Can we split horizontally?
|
|
((window-splittable-p window t)
|
|
(/ body-width 2))
|
|
;; In worst case, just use the same width of current window
|
|
(t body-width))))
|
|
|
|
(provide 'lean-flycheck)
|