feat(emacs): add lean-flycheck-turn-on/off/toggle

src/emacs/lean-flycheck.el

@@ -4,14 +4,23 @@
 ;; Author: Soonho Kong
 ;;
 
-(when lean-use-flycheck
+(defvar-local lean-flycheck-initialized nil
+  "Return true if lean-flycheck has been initialized")
+(defvar-local lean-flycheck-lmake-name "lmake"
+  "lmake name")
+(defvar-local lean-flycheck-lmake-options "--flycheck"
+  "flycheck option for lean")
+
+(defun lean-flycheck-init ()
+  "Initialize lean-flychek checker"
+  (unless lean-flycheck-initialized
     (require 'flycheck)
-  (setq-local lean-lmake-name "lmake")
-  (setq-local lean-lmake-options "--flycheck")
     (eval
      `(flycheck-define-checker lean-checker-file
         "A Lean syntax checker (file)."
-      :command (,(lean-get-executable lean-lmake-name) ,lean-lmake-options source-inplace)
+        :command (,(lean-get-executable lean-flycheck-lmake-name)
+                  ,lean-flycheck-lmake-options
+                  source-inplace)
         :error-patterns
         ((error line-start "FLYCHECK_BEGIN ERROR\n"
                 (file-name) ":" line ":" column  ": error: "
@@ -28,5 +37,32 @@
         (lambda () (and buffer-file-name
                    (string= "lean" (file-name-extension buffer-file-name))))))
     (add-to-list 'flycheck-checkers 'lean-checker-file)
-  (add-hook 'lean-mode-hook '(lambda () (flycheck-mode t))))
+    (setq lean-flycheck-initialized t)))
+
+(defun lean-flycheck-turn-on ()
+  (interactive)
+  (unless lean-flycheck-use
+    (when (interactive-p)
+      (message "use flycheck in lean-mode"))
+    (setq lean-flycheck-use t))
+  (lean-flycheck-init)
+  (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)))
+
+(add-hook 'lean-mode-hook '(lambda ()
+             (when lean-flycheck-use (lean-flycheck-turn-on))))
+
 (provide 'lean-flycheck)

src/emacs/lean-settings.el

@@ -30,7 +30,7 @@
   :group 'lean
   :type 'string)
 
-(defcustom lean-use-flycheck t
+(defcustom lean-flycheck-use t
   "Use flycheck for lean."
   :group 'lean
   :type 'boolean)