Add proof-script-imenu-generic-expression for configuring imenu.

2 files changed, 14 insertions, 3 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 0450d8f2..6f93e807 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1133,6 +1133,15 @@ default."
   :type 'function
   :group 'proof-script)
 
+
+(defcustom proof-script-imenu-generic-expression nil
+  "Regular expressions to help find definitions and proofs in a script.
+Value for `imenu-generic-expression', see documentation of Imenu
+and that variable for details."
+  :type 'sexp
+  :group 'proof-script)
+
+
 ;; FIXME da: This next one is horrible.  We clearly would rather
 ;; have just proof-goal-command regexp instead.  This was born to solve
 ;; problem that Coq can have goals which look like definitions, etc.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 48465b82..2ec6bc56 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2811,19 +2811,21 @@ Choice of function depends on configuration setting."
 
 
 (defun proof-setup-imenu ()
-  "Setup a default for imenu."
+  "Setup a default for imenu, perhaps using `proof-script-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
+	 (or 
+	  proof-script-imenu-generic-expression
+	     (delq nil
 	       (list
 		(if proof-goal-with-hole-regexp
 		    (list nil proof-goal-with-hole-regexp
 			  proof-goal-with-hole-result))
 		(if proof-save-with-hole-regexp
 		    (list "Saves" proof-save-with-hole-regexp
-			  proof-save-with-hole-result)))))))
+			  proof-save-with-hole-result))))))))
 
 (defun proof-setup-func-menu ()
   "Configure func-menu for a proof script buffer."