From 0457fdc1c6f9634bf38e43eb3219ee7f8ad4f16b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 14 Apr 2004 09:52:36 +0000
Subject: Space in named entities popup

---
 generic/proof-script.el | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'generic/proof-script.el')

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
-- 
cgit v1.2.3