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

feat(lean4-mode/lean4-flycheck): add lean4-bootstrapped-checker

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-20 12:59:18 +01:00
parent 32a3c0e62e
commit 72274870ef
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
lean4-mode/lean4-flycheck.el
View file

@ -19,13 +19,15 @@
(t (flycheck-mode 1))))
(defun lean4-flycheck-command ()
"Concat lean4-flychecker-checker-name with options"
(let ((command
(-concat `(,(lean4-get-executable lean4-executable-name))
lean4-extra-arguments
'("--json" "--make" "--stdin"))))
command))
(defun lean4-bootstrapped-flycheck-command ()
`(,(s-concat (lean4-get-executable lean4-executable-name) "-bootstrapped") source-inplace))
(cl-defun lean4-flycheck-parse-task (checker buffer cur-file-name
&key pos_line pos_col desc file_name &allow-other-keys)
(if (equal cur-file-name file_name)
@ -99,13 +101,18 @@
(lean4-server-session-messages lean4-server-session))))))))
(defun lean4-flycheck-init ()
"Initialize lean4-flychek checker"
"Initialize lean4-flycheck checker"
(flycheck-define-command-checker 'lean4-checker
"A Lean syntax checker."
:command (lean4-flycheck-command)
:standard-input t
:error-parser #'lean4-flycheck-parse-errors
:modes '(lean4-mode))
(flycheck-define-command-checker 'lean4-bootstrapped-checker
"Bootstrapped Lean syntax checker."
:command (lean4-bootstrapped-flycheck-command)
:error-parser #'lean4-flycheck-parse-errors
:modes '(lean4-mode))
(add-to-list 'flycheck-checkers 'lean4-checker))
(defun lean4-flycheck-turn-on ()