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

feat(emacs/lean-mode.el): use whitespace-cleanup-mode to fci-mode

Browse source
This commit is contained in:
Soonho Kong 2014-08-07 08:02:27 -07:00
parent f9f8c09143
commit f523c25c52
1 changed files with 10 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -8,28 +8,13 @@
(require 'compile) (require 'compile)
(require 'flymake) (require 'flymake)
(require 'flycheck) (require 'flycheck)
(require 'fill-column-indicator)
(require 'whitespace-cleanup-mode)
(require 'lean-util) (require 'lean-util)
(require 'lean-settings) (require 'lean-settings)
(require 'lean-flycheck) (require 'lean-flycheck)
(require 'lean-input) (require 'lean-input)
(defun lean-get-rootdir ()
(lean-get-this-if-true-or-that
lean-rootdir
(error "'lean-rootdir' is not defined. Please have\
(customize-set-variable 'lean-rootdir \"~/work/lean\")\
in your emacs configuration.\
Also make sure that your (custom-set-variable ...) comes before\
(require 'lean-mode).")))
(defun lean-get-executable (exe-name)
"Return fullpath of lean executable"
(let ((lean-binary-dir-name "bin"))
(when lean-rootdir
(concat (file-name-as-directory (lean-get-rootdir))
(file-name-as-directory "bin")
exe-name))))
(defun lean-compile-string (exe-name args file-name) (defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name" "Concatenate exe-name, args, and file-name"
(format "%s %s %s" exe-name args file-name)) (format "%s %s %s" exe-name args file-name))
@ -95,12 +80,18 @@ Also make sure that your (custom-set-variable ...) comes before\
(lean-set-keys) (lean-set-keys)
(setq local-abbrev-table lean-mode-abbrev-table) (setq local-abbrev-table lean-mode-abbrev-table)
(abbrev-mode 1) (abbrev-mode 1)
(when (and lean-rule-column
lean-show-rule-column-method)
(case lean-show-rule-column-method
('vline (setq fci-rule-column lean-rule-column)
(add-hook 'lean-mode-hook 'fci-mode))))
(if lean-delete-trailing-whitespace
(add-hook 'lean-mode-hook 'whitespace-cleanup-mode)
(remove-hook 'lean-mode-hook 'whitespace-cleanup-mode))
)) ))
"A mode for Lean files" ;; doc string for this mode "A mode for Lean files" ;; doc string for this mode
) )
(provide 'lean-mode) (provide 'lean-mode)
; (regexp-opt '("Int" "Bool" "Nat" "Type" "Real") t) ; (regexp-opt '("Int" "Bool" "Nat" "Type" "Real") t)
; (regexp-opt '("let" "in" "have" "calc" "forall" "exists") t) ; (regexp-opt '("let" "in" "have" "calc" "forall" "exists") t)
; (regexp-opt '("=" "->" "≠" "∨" "∧" "¬" "/\\" "\\/" "+" "-" "*" "/" "<" ">" "≤" "≥" "==" "∀" "∃" "→" "λ" ":") t) ; (regexp-opt '("=" "->" "≠" "∨" "∧" "¬" "/\\" "\\/" "+" "-" "*" "/" "<" ">" "≤" "≥" "==" "∀" "∃" "→" "λ" ":") t)