From 72274870ef6903e50fbb1227e48e4b40aeac0ab1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Dec 2018 12:59:18 +0100 Subject: [PATCH] feat(lean4-mode/lean4-flycheck): add `lean4-bootstrapped-checker` --- lean4-mode/lean4-flycheck.el | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/lean4-mode/lean4-flycheck.el b/lean4-mode/lean4-flycheck.el index 9af32094ee..44fd6c0b56 100644 --- a/lean4-mode/lean4-flycheck.el +++ b/lean4-mode/lean4-flycheck.el @@ -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 ()