michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(emacs/lean-mode.el): add configuration menu-item for flycheck

Browse source 
close #451
This commit is contained in:
Soonho Kong 2015-03-05 14:42:59 -05:00
parent b7c852a5c8
commit 87c236613a
2 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/emacs/lean-flycheck.el
View file

@ -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

11
src/emacs/lean-mode.el
View file

@ -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]))