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

chore(emacs): move lean-choose-minor-mode-based-on-extension to lean-util.el

Browse source
This commit is contained in:
Soonho Kong 2015-02-10 12:54:32 -05:00
parent dcee8ddb1f
commit 46d99c8077
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -152,16 +152,6 @@ enabled and disabled respectively.")
(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-choose-minor-mode-based-on-extension ()
;; Based on the extension of buffer, return either 'HoTT or 'Standard
(interactive)
(let ((file-name (buffer-file-name)))
(cond ((s-ends-with? ".lean" file-name)
'Standard)
((s-ends-with? ".hlean" file-name)
'HoTT)
(t 'Standard))))
(defun lean-mode-setup ()
"Default lean-mode setup"
;; Flycheck

10
src/emacs/lean-util.el
View file

@ -184,4 +184,14 @@
(when lean-delete-trailing-whitespace
(delete-trailing-whitespace)))
(defun lean-choose-minor-mode-based-on-extension ()
;; Based on the extension of buffer, return either 'hott or 'standard
(interactive)
(let ((file-name (buffer-file-name)))
(cond ((s-ends-with? ".lean" file-name)
'standard)
((s-ends-with? ".hlean" file-name)
'hott)
(t 'standard))))
(provide 'lean-util)