diff --git a/src/emacs/README.md b/src/emacs/README.md index 9046bb40e..82511e9d7 100644 --- a/src/emacs/README.md +++ b/src/emacs/README.md @@ -1,20 +1,40 @@ lean-mode ========= +Emacs mode for [lean theorem prover][lean] + +[lean]: https://github.com/leanprover/lean + Requirement ----------- - - [Emacs 24][emacs24] +``lean-mode`` requires [Emacs 24][emacs24] and following (optional) +packages which can be installed via ``M-x package-install``. + - [flycheck][flycheck] - [fill-column-indicator][fci] + - [whitespace-cleanup-mode][wcm] + +To install them, you need to have [MELPA][MELPA] in your +``package-archives``. You can add it by evaluating the following elisp +code: + +```elisp +(add-to-list 'package-archives + '("marmalade" . "http://marmalade-repo.org/packages/") t) +``` [emacs24]: http://www.gnu.org/software/emacs/ [flycheck]: http://flycheck.readthedocs.org/en/latest/ [fci]: https://github.com/alpaker/Fill-Column-Indicator +[wcm]: https://github.com/purcell/whitespace-cleanup-mode +[MELPA]: http://melpa.milkbox.net/ Setup ----- +Put the following elisp code on your emacs setup: + ```elisp (setq lean-rootdir "~/projects/lean") (setq-local lean-emacs-path @@ -24,7 +44,7 @@ Setup (add-to-list 'load-path (expand-file-name lean-emacs-path)) (require 'lean-mode) -;; customization +;; lean customization (customize-set-variable 'lean-show-rule-column-method 'vline) (customize-set-variable 'lean-rule-column 100) (customize-set-variable 'lean-delete-trailing-whitespace t) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index a51863d3e..3b26f32ba 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -38,14 +38,6 @@ written." :group 'lean :type 'boolean) -(and lean-delete-trailing-whitespace - (cond - ; If white-space-cleanup-mode exists, use it - (((fboundp whitespace-cleanup-mode) - (add-hook 'lean-mode-hook 'whitespace-cleanup-mode)) - ; Otherwise - (t (add-hook 'write-file-functions 'whitespace-cleanup))))) - (defcustom lean-rule-column 100 "Specify rule-column." :group 'lean