From 87c236613aaa42bc5b8a90d5c9d680091a5a61a9 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 5 Mar 2015 14:42:59 -0500
Subject: [PATCH] feat(emacs/lean-mode.el): add configuration menu-item for
 flycheck

close #451
---
 src/emacs/lean-flycheck.el |  7 +++++++
 src/emacs/lean-mode.el     | 11 +++++++----
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 91846083c..2b4019d4b 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -7,6 +7,13 @@
 (require 'lean-settings)
 (require 'lean-option)
 
+(defun lean-toggle-flycheck-mode ()
+  "Toggle flycheck-mode"
+  (interactive)
+  (cond
+   (flycheck-mode (flycheck-mode -1))
+   (t             (flycheck-mode  1))))
+
 (defun lean-flycheck-command ()
   "Concat lean-flychecker-checker-name with options"
   (let ((command
diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 66089b643..c2199892a 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -107,20 +107,23 @@
     ["Execute lean"         lean-execute                      t]
     ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
     "-----------------"
-    ["Show type info"       lean-show-type lean-eldoc-use]
+    ["Show type info"       lean-show-type                    (and lean-eldoc-use eldoc-mode)]
     ["Fill a placeholder"   lean-fill-placeholder             (looking-at  (rx symbol-start "_"))]
     ["Find tag at point"    lean-find-tag                     t]
     ["Global tag search"    lean-global-search                t]
     "-----------------"
-    ["Run flycheck"         flycheck-compile                  lean-flycheck-use]
-    ["List of errors"       flycheck-list-errors              lean-flycheck-use]
+    ["Run flycheck"         flycheck-compile                  (and lean-flycheck-use flycheck-mode)]
+    ["List of errors"       flycheck-list-errors              (and lean-flycheck-use flycheck-mode)]
     "-----------------"
     ["Clear all cache"      lean-clear-cache                  t]
     ["Kill lean process"    lean-server-kill-process          t]
     ["Restart lean process" lean-server-restart-process       t]
     "-----------------"
     ("Configuration"
-     ["Show type at point" lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
+     ["Use flycheck (on-the-fly syntax check)"
+      lean-toggle-flycheck-mode :active t :style toggle :selected flycheck-mode]
+     ["Show type at point"
+      lean-toggle-eldoc-mode :active t :style toggle :selected eldoc-mode])
     "-----------------"
     ["Customize lean-mode" (customize-group 'lean)            t]))