From 0ac1ec1de3d1b1fadf69505d9bce81f379ac8da2 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Mon, 8 Sep 2014 11:39:20 -0700 Subject: [PATCH] feat(emacs/lean-settings): add lean-show-only-type-in-parens Fix #135 --- src/emacs/lean-info.el | 7 ++++--- src/emacs/lean-settings.el | 4 ++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/emacs/lean-info.el b/src/emacs/lean-info.el index 010b89b13..2ff647407 100644 --- a/src/emacs/lean-info.el +++ b/src/emacs/lean-info.el @@ -588,9 +588,10 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim." ", "))) (when extra (setq str - (format "(%s) : %s" - (propertize (lean-info-extra-expr-str extra) 'face 'font-lock-variable-name-face) - (lean-info-extra-type-str extra)))) + (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)))))) (when (and name-str type-str) (setq str (format "%s : %s" (propertize name-str 'face 'font-lock-variable-name-face) diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el index 78badc556..10ef6af29 100644 --- a/src/emacs/lean-settings.el +++ b/src/emacs/lean-settings.el @@ -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