lean2/src/emacs/lean-flycheck.el

;; 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-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 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)