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

fix(lean4-mode/lean4-flycheck): update lean4-bootstrapped-checker

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-24 20:54:41 +01:00
parent 082b217928
commit 88af3c948a
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -18,16 +18,14 @@
(flycheck-mode (flycheck-mode -1))
(t (flycheck-mode 1))))
(defun lean4-flycheck-command ()
(defun lean4-flycheck-command (extra-args)
(let ((command
(-concat `(,(lean4-get-executable lean4-executable-name))
'((eval lean4-extra-arguments))
extra-args
'("--json" "--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)
@ -104,13 +102,14 @@
"Initialize lean4-flycheck checker"
(flycheck-define-command-checker 'lean4-checker
"A Lean syntax checker."
:command (lean4-flycheck-command)
: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)
:command (lean4-flycheck-command '("--new-frontend"))
:standard-input t
:error-parser #'lean4-flycheck-parse-errors
:modes '(lean4-mode))
(add-to-list 'flycheck-checkers 'lean4-checker))