aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-14 09:52:36 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-14 09:52:36 +0000
commit0457fdc1c6f9634bf38e43eb3219ee7f8ad4f16b (patch)
tree58f7a31e6cbd9daf6cafa4dcb6d8a74b80624ad8
parent39697b7a1e8077e8d93a0a0d231388c2ff232a66 (diff)
Space in named entities popup
-rw-r--r--generic/proof-script.el7
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 9e8d34b5..48465b82 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -680,7 +680,7 @@ NAME does not need to be unique."
(concat (upcase-initials (symbol-name idiom))
(if (and name
(not (equal name proof-unnamed-theorem-name)))
- (concat "[" name "]"))))
+ (concat " [" name "]"))))
((or (eq type 'proof) (eq type 'goalsave))
(concat "Proof"
(let ((name (span-property span 'name)))
@@ -2812,8 +2812,9 @@ Choice of function depends on configuration setting."
(defun proof-setup-imenu ()
"Setup a default for imenu."
- (unless (and (boundp 'imenu-generic-expression)
- imenu-generic-expression)
+ (unless ;; already setup, leave it alone
+ (and (boundp 'imenu-generic-expression)
+ imenu-generic-expression)
(set (make-local-variable 'imenu-generic-expression)
(delq nil
(list