From 07e188acdbce5e7974571ca5541ac4522885fd68 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Thu, 7 Aug 2014 10:37:25 -0700
Subject: [PATCH] feat(emacs/README.md): add instr. for MELPA; add
 whitespace-cleanup-mode

---
 src/emacs/README.md        | 24 ++++++++++++++++++++++--
 src/emacs/lean-settings.el |  8 --------
 2 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/src/emacs/README.md b/src/emacs/README.md
index 9046bb40e7..82511e9d79 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 a51863d3e0..3b26f32ba0 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