From b650793b3389dacfd0ab819988249a66039e2cfe Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Mon, 15 Sep 2014 13:02:45 -0700
Subject: [PATCH] feat(lean-option): handle default pp.width option value

---
 src/emacs/lean-option.el   | 4 ++++
 src/emacs/lean-settings.el | 6 +++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/emacs/lean-option.el b/src/emacs/lean-option.el
index f2c57aab2..a6336265d 100644
--- a/src/emacs/lean-option.el
+++ b/src/emacs/lean-option.el
@@ -21,6 +21,10 @@
     (string-join str-list "\n")))
 
 (defun lean-option-string ()
+  "Return string of Lean options set by lean-set-option command"
+  (let ((pp-width-entry (assoc-string "pp.width" lean-global-option-alist)))
+    (unless pp-width-entry
+      (lean-update-option-alist "pp.width" lean-default-pp-width)))
   (when lean-global-option-alist
     (--reduce (format "%s %s" acc it)
             (--map (format "-D%s=%s" (car it) (cdr it))
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index caa575961..7d565bef8 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -70,13 +70,13 @@ show both of expressions and types.")
   :group 'lean
   :type 'int)
 
-(defcustom lean-flycheck-pp-width 120
-  "Width of flycheck error messages (Restart required to be effective)"
+(defcustom lean-default-pp-width 120
+  "Width of Lean error/warning messages"
   :group 'lean
   :type 'int)
 
 (defcustom lean-flycheck-checker-options
-  `("--flycheck" ,(format "%d" lean-flycheck-pp-width)
+  `("--flycheck"
     "--flycheck-max-messages" ,(format "%d" lean-flycheck-max-messages-to-display))
   "lean-flychecker checker option"
   :group 'lean)