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

feat(lean-option): handle default pp.width option value

Browse source
This commit is contained in:
Soonho Kong 2014-09-15 13:02:45 -07:00
parent 254d861970
commit b650793b33
2 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-option.el
View file

@ -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))

6
src/emacs/lean-settings.el
View file

@ -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)