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

feat(emacs/lean-settings): add 'lean-follow-changes' option

Browse source
This commit is contained in:
Soonho Kong 2014-10-29 23:57:54 -07:00
parent 84b516994c
commit b7d805a145
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -125,8 +125,6 @@
'(
;; Handle events that may start automatic syntax checks
(after-save-hook . lean-server-after-save)
(after-change-functions . lean-after-change-function)
(before-change-functions . lean-before-change-function)
;; ;; Handle events that may triggered pending deferred checks
;; (window-configuration-change-hook . lean-perform-deferred-syntax-check)
;; (post-command-hook . lean-perform-deferred-syntax-check)
@ -149,6 +147,10 @@ The `car' of each pair is a hook variable, the `cdr' a function
to be added or removed from the hook variable if Flycheck mode is
enabled and disabled respectively.")
(when lean-follow-changes
(add-to-list 'lean-hooks-alist '(after-change-functions . lean-after-change-function))
(add-to-list 'lean-hooks-alist '(before-change-functions . lean-before-change-function)))
(defun lean-mode-setup ()
"Default lean-mode setup"
;; Flycheck

4
src/emacs/lean-settings.el
View file

@ -141,4 +141,8 @@ false (nil)."
(const :tag "Show only the first" show-first)
(const :tag "Show the first goal, and the conclusions of all other goals" show-first-and-other-conclusions)))
(defcustom lean-follow-changes 't
"Disable this if we don't need to keep track of the changes. A usage
is to batch-process .org files to .html files")
(provide 'lean-settings)