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

feat(emacs/lean-settings): add lean-show-only-type-in-parens

Browse source 
Fix #135
This commit is contained in:
Soonho Kong 2014-09-08 11:39:20 -07:00
parent a40894a712
commit 0ac1ec1de3
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/emacs/lean-info.el
View file

@ -588,9 +588,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
", ")))
(when extra
(setq str
(format "(%s) : %s"
(cond (lean-show-only-type-in-parens (format ": %s" (lean-info-extra-type-str extra)))
(t (format "(%s) : %s"
(propertize (lean-info-extra-expr-str extra) 'face 'font-lock-variable-name-face)
(lean-info-extra-type-str extra))))
(lean-info-extra-type-str extra))))))
(when (and name-str type-str)
(setq str (format "%s : %s"
(propertize name-str 'face 'font-lock-variable-name-face)

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

@ -60,6 +60,10 @@
"lean-flychecker checker option"
:group 'lean)
(defcustom lean-show-only-type-in-parens t
"Show only types of expression in parens if non-nil. Otherwise,
show both of expressions and types.")
(defcustom lean-delete-trailing-whitespace nil
"Set this variable to true to automatically delete trailing
whitespace when a buffer is loaded from a file or when it is