feat(emacs/README.md): add instr. for MELPA; add whitespace-cleanup-mode
This commit is contained in:
parent
a2867b3d06
commit
07e188acdb
2 changed files with 22 additions and 10 deletions
|
@ -1,20 +1,40 @@
|
||||||
lean-mode
|
lean-mode
|
||||||
=========
|
=========
|
||||||
|
|
||||||
|
Emacs mode for [lean theorem prover][lean]
|
||||||
|
|
||||||
|
[lean]: https://github.com/leanprover/lean
|
||||||
|
|
||||||
Requirement
|
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]
|
- [flycheck][flycheck]
|
||||||
- [fill-column-indicator][fci]
|
- [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/
|
[emacs24]: http://www.gnu.org/software/emacs/
|
||||||
[flycheck]: http://flycheck.readthedocs.org/en/latest/
|
[flycheck]: http://flycheck.readthedocs.org/en/latest/
|
||||||
[fci]: https://github.com/alpaker/Fill-Column-Indicator
|
[fci]: https://github.com/alpaker/Fill-Column-Indicator
|
||||||
|
[wcm]: https://github.com/purcell/whitespace-cleanup-mode
|
||||||
|
[MELPA]: http://melpa.milkbox.net/
|
||||||
|
|
||||||
Setup
|
Setup
|
||||||
-----
|
-----
|
||||||
|
|
||||||
|
Put the following elisp code on your emacs setup:
|
||||||
|
|
||||||
```elisp
|
```elisp
|
||||||
(setq lean-rootdir "~/projects/lean")
|
(setq lean-rootdir "~/projects/lean")
|
||||||
(setq-local lean-emacs-path
|
(setq-local lean-emacs-path
|
||||||
|
@ -24,7 +44,7 @@ Setup
|
||||||
(add-to-list 'load-path (expand-file-name lean-emacs-path))
|
(add-to-list 'load-path (expand-file-name lean-emacs-path))
|
||||||
(require 'lean-mode)
|
(require 'lean-mode)
|
||||||
|
|
||||||
;; customization
|
;; lean customization
|
||||||
(customize-set-variable 'lean-show-rule-column-method 'vline)
|
(customize-set-variable 'lean-show-rule-column-method 'vline)
|
||||||
(customize-set-variable 'lean-rule-column 100)
|
(customize-set-variable 'lean-rule-column 100)
|
||||||
(customize-set-variable 'lean-delete-trailing-whitespace t)
|
(customize-set-variable 'lean-delete-trailing-whitespace t)
|
||||||
|
|
|
@ -38,14 +38,6 @@ written."
|
||||||
:group 'lean
|
:group 'lean
|
||||||
:type 'boolean)
|
: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
|
(defcustom lean-rule-column 100
|
||||||
"Specify rule-column."
|
"Specify rule-column."
|
||||||
:group 'lean
|
:group 'lean
|
||||||
|
|
Loading…
Reference in a new issue