From acd15627e674868023435efda702bded80c835d9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 14 Apr 2004 10:33:51 +0000 Subject: Add proof-script-imenu-generic-expression for configuring imenu. --- generic/proof-config.el | 9 +++++++++ generic/proof-script.el | 8 +++++--- 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." -- cgit v1.2.3