Renamed proof-mode-name -> proof-general-name.

Reimplemented configuration for fume-menu.
Now works for named goals, named saves, and (e.g. lego) both!
Removed some FIXME's.

4 files changed, 234 insertions, 64 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index d76b7fcc..1207163d 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -407,20 +407,90 @@ The script buffer's comment-end is set to this string plus a space."
 (defcustom proof-save-command-regexp nil 
   "Matches a save command"
   :type 'regexp
-  :group 'prover-config)
+  :group 'proof-script)
 
 (defcustom proof-save-with-hole-regexp nil 
   "Regexp which matches a command to save a named theorem.
-Match number 2 should be the name of the theorem saved."
+Match number 2 should be the name of the theorem saved.
+Used for setting names of goal..save regions and for default
+func-menu configuration in proof-script-find-next-goalsave."
+  :type 'regexp
+  :group 'proof-script)
+
+(defcustom proof-goal-command-regexp nil
+  "Matches a goal command."
   :type 'regexp
   :group 'proof-script)
 
 (defcustom proof-goal-with-hole-regexp nil 
   "Regexp which matches a command used to issue and name a goal.
-Match number 2 should be the name of the goal issued."
+Match number 2 should be the name of the goal issued.
+Used for setting names of goal..save regions and for default
+func-menu configuration in proof-script-find-next-goalsave."
   :type 'regexp
   :group 'proof-script)
 
+(defcustom proof-script-next-entity-regexps nil
+  "Regular expressions to control finding definitions in script.
+This is the list of the form
+
+   (ANYENTITY-REGEXP
+    DISCRIMINATOR-REGEXP  ... DISCRIMINATOR-REGEXP)
+
+The idea is that ANYENTITY-REGEXP matches any named entity in the
+proof script, on a line where the name appears.  This is assumed to be
+the start or the end of the entity.  The discriminators then test
+which kind of entity has been found, to get its name.  A
+DISCRIMINATOR-REGEXP has one of the forms
+
+  (REGEXP MATCHNO) 
+  (REGEXP MATCHNO 'backward BACKREGEXP) 
+  (REGEXP MATCHNO 'forward FORWARDREGEXP)
+
+If REGEXP matches the string captured by ANYENTITY-REGEXP, then
+MATCHNO is the match number for the substring which names the entity.
+
+If 'backward BACKREGEXP is present, then the start of the entity
+is found by searching backwards for BACKREGEXP.
+
+Conversely, if 'forward FORWARDREGEXP is found, then the end of
+the entity is found by searching forwards for FORWARDREGEXP.
+
+Otherwise, the start and end of the entity will be the region matched
+by ANYENTITY-REGEXP.
+
+This mechanism allows fairly complex parsing of the buffer, in
+particular, it allows for goal..save regions which are named only at
+the end.  However, it does not parse strings, comments. or parentheses.
+
+A default value which should work for goal..saves is calculated from
+proof-goal-with-hole-regexp, proof-goal-command-regexp, and
+proof-save-with-hole-regexp."
+  :type 'sexp
+    ;; Bit tricky.
+    ;; (list (regexp :tag "Any entity matcher")
+    ;;    (:inline t repeat (choice regexp (const 'backward) etc
+  :group 'proof-script)
+
+
+(defcustom proof-script-find-next-entity-fn
+  'proof-script-find-next-entity
+  "Name of function to find next interesting entity in a script buffer.
+This is used to configure func-menu.  The default value is
+proof-script-find-next-entity, which searches for the next entity
+based on fume-function-name-regexp which by default is set from
+proof-script-next-entity-regexps.  The function should move
+point forward in a buffer, and return a cons cell of the name and the
+beginning of the entity's region."
+  :type 'function
+  :group 'proof-script)
+
+;; FIXME da: This next one is horrible.  We clearly would rather
+;; have proof-goal-regexp instead.  I think this was born to
+;; solve func-menu configuration for Coq (or a similar problem),
+;; but now that can be configured in a better way.
+;; This function variable needs removing.
+
 (defcustom proof-goal-command-p nil 
   "Is this a goal"
   :type 'function
@@ -739,9 +809,8 @@ data triggered by `proof-shell-retract-files-regexp'."
 ;;
 ;; 6. Global constants
 ;; 
-(defcustom proof-mode-name "Proof-General"
-  "Root name for proof script mode.  
-Used internally and in menu titles."
+(defcustom proof-general-name "Proof-General"
+  "Proof General name used internally and in menu titles."
   :type 'string
   :group 'proof-general-internals)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e242eda4..58171648 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -50,27 +50,80 @@
 
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; A few small utilities					    ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Configuration of func-menu ("fume")	
+;;
+;; This code is only enabled if the user loads func-menu into Emacs.
+;;
+
+(eval-after-load "func-menu"	'(progn	; BEGIN if func-menu
+;; BEGIN OLD
+;; FIXME da: wasn't this supposed to return a cons of a string
+;; and a buffer position?
+;(defun proof-match-find-next-function-name (buffer)
+;  "General next function name in BUFFER finder using match.
+;The regexp is assumed to be a two item list the car of which is the regexp
+;to use, and the cdr of which is the match position of the function
+;name. Moves point after the match.
+
+;The package fume-func provides the function
+;`fume-match-find-next-function-name' with the same specification.
+;However, fume-func's version is incorrect"
+;  ;; DO NOT USE save-excursion; we need to move point!
+;  ;; save-excursion is called at a higher level in the func-menu
+;  ;; package 
+;    (set-buffer buffer)
+;    (let ((r (car fume-function-name-regexp))
+;	  (p (cdr fume-function-name-regexp)))
+;      (and (re-search-forward r nil t)
+;	   (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))
+;; END OLD.
+
+;; This is actually a fairly general function.
+
+(deflocal proof-script-last-entity nil
+  "Record of last entity found.   A hack for entities that are named
+in two places, so that find-next-entity doesn't return the same values
+twice.")
+
+(defun proof-script-find-next-entity (buffer)
+  "Find the next entity for function menu in a proof script.
+A value for fume-find-function-name-method-alist for proof scripts.
+Uses fume-function-name-regexp, which is intialised from 
+proof-script-next-entity-regexps, which see."
+  ;; Hopefully this function is fast enough.
+  (set-buffer buffer)
+  ;;  could as well use next-entity-regexps directly since this is
+  ;;  not really meant to be used as a general function. 
+  (let ((anyentity	(car fume-function-name-regexp)))
+    (if (re-search-forward anyentity nil t)
+	;; We've found some interesting entity, but have to find out
+	;; which one, and where it begins.  
+	(let ((entity (buffer-substring (match-beginning 0) (match-end 0)))
+	      (start (match-beginning 0))
+	      (discriminators (cdr fume-function-name-regexp))
+	      (p (point))
+	      disc res)
+	  (while (and (not res) (setq disc (car-safe discriminators)))
+	    (if (string-match (car disc) entity)
+		(let ((name (substring
+			     entity
+			     (match-beginning (nth 1 disc))
+			     (match-end (nth 1 disc)))))
+		  (cond
+		   ((eq (nth 2 disc) 'backward)
+		    (setq start
+			  (or (re-search-backward (nth 3 disc) nil t)
+			      start))
+		    (goto-char p))
+		   ((eq (nth 2 disc) 'forward)
+		    (re-search-forward (nth 3 disc))))
+		  (setq res (cons name start)))
+	      (setq discriminators (cdr discriminators))))
+	  res))))
+
+))					; END if func-menu
 
-(defun proof-match-find-next-function-name (buffer)
-  "General next function name in BUFFER finder using match.
-The regexp is assumed to be a two item list the car of which is the regexp
-to use, and the cdr of which is the match position of the function
-name. Moves point after the match.
-
-The package fume-func provides the function
-`fume-match-find-next-function-name' with the same specification.
-However, fume-func's version is incorrect"
-  ;; DO NOT USE save-excursion; we need to move point!
-  ;; save-excursion is called at a higher level in the func-menu
-  ;; package 
-    (set-buffer buffer)
-    (let ((r (car fume-function-name-regexp))
-	  (p (cdr fume-function-name-regexp)))
-      (and (re-search-forward r nil t)
-	   (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))
 
 
 
@@ -78,12 +131,6 @@ However, fume-func's version is incorrect"
 ;; Basic code for the locked region and the queue region            ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; FIXME da: remove this dead code 
-;; (defvar proof-locked-hwm nil
-;;  "Upper limit of the locked region")
-;; (defvar proof-queue-loose-end nil
-;;  "Limit of the queue region that is not equal to proof-locked-hwm.")
-
 (deflocal proof-locked-span nil
   "The locked span of the buffer.")
 
@@ -93,7 +140,6 @@ However, fume-func's version is incorrect"
 ;; So nasty things might happen if a locked file is visited whilst
 ;; another buffer has a non-empty queue region being processed.
 
-
 (deflocal proof-queue-span nil
   "The queue span of the buffer.")
 
@@ -408,9 +454,6 @@ the hooks `proof-activate-scripting-hook' are run."
 
 
 
-
-
-
 
 ;;; begin messy COMPATIBILITY HACKING for FSFmacs.
 ;;; 
@@ -1432,7 +1475,7 @@ sent to the assistant."
 ;;;###autoload
 (eval-and-compile			; to define vars
 (define-derived-mode proof-mode fundamental-mode 
-  proof-mode-name
+  proof-general-name
   "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
   (setq proof-buffer-type 'script)
@@ -1494,20 +1537,6 @@ finish setup which depends on specific proof assistant configuration."
   (setq comment-start-skip 
     (concat (regexp-quote proof-comment-start) "+\\s_?"))
 
-  ;; func-menu --- Jump to a goal within a buffer
-  ;; FIXME 1: is there any way to get this to work for named saves
-  ;; instead of named goals?
-  ;; FIXME 2: each time proof mode is entered these extensions are
-  ;; made!  Probably needs moving out of this function.
-  (and (boundp 'fume-function-name-regexp-alist)
-       (defvar fume-function-name-regexp-proof
-	 (cons proof-goal-with-hole-regexp 2))
-       (push (cons major-mode 'fume-function-name-regexp-proof)
-	     fume-function-name-regexp-alist))
-  (and (boundp 'fume-find-function-name-method-alist)
-       (push (cons major-mode 'proof-match-find-next-function-name)
-	     fume-find-function-name-method-alist))
-
   ;; Additional key definitions which depend on configuration for
   ;; specific proof assistant.
   (define-key proof-mode-map
@@ -1529,7 +1558,7 @@ finish setup which depends on specific proof assistant configuration."
   (easy-menu-define proof-mode-menu  
 		    proof-mode-map
 		    "Menu used in Proof General scripting mode."
-		    (cons proof-mode-name
+		    (cons proof-general-name
 			  (append
 			   (cdr proof-menu)
 			   ;; begin UGLY COMPATIBILTY HACK
@@ -1566,9 +1595,62 @@ finish setup which depends on specific proof assistant configuration."
   (and (boundp 'font-lock-always-fontify-immediately)
        (setq font-lock-always-fontify-immediately t))
 
+  ;; Make sure func menu is configured.  (NB: Ideal place for this and
+  ;; similar stuff would be in something evaluated at top level after
+  ;; defining the derived mode: normally we wouldn't repeat this
+  ;; each time the mode function is run, so we wouldn't need "pushnew").
+
+  (cond ((featurep 'func-menu)
+	 (unless proof-script-next-entity-regexps ; unless already set
+	   ;; Try to calculate a useful default value.
+	   ;; FIXME: this is rather complicated!  The use of the regexp
+	   ;; variables needs sorting out. 
+	     (customize-set-variable
+	      'proof-script-next-entity-regexps
+	      (let ((goal-discrim
+		     ;; Goal discriminator searches forward for matching
+		     ;; save if the regexp is set.
+		     (if proof-goal-with-hole-regexp
+			 (if proof-save-command-regexp
+			     (list
+			      proof-goal-with-hole-regexp 2
+			      'forward proof-save-command-regexp)
+			   (list proof-goal-with-hole-regexp 2))))
+		    ;; Save discriminator searches backward for matching
+		    ;; goal if the regexp is set.
+		    (save-discrim
+		     (if proof-save-with-hole-regexp
+			 (if proof-goal-command-regexp
+			     (list
+			      proof-save-with-hole-regexp 2
+			      'backward proof-goal-command-regexp)
+			   (list proof-save-with-hole-regexp 2)))))
+		(cond
+		 ((and proof-goal-with-hole-regexp proof-save-with-hole-regexp)
+		  (list
+		   (proof-regexp-alt
+		    proof-goal-with-hole-regexp
+		    proof-save-with-hole-regexp) goal-discrim save-discrim))
+		  
+		 (proof-goal-with-hole-regexp
+		  (list proof-goal-with-hole-regexp goal-discrim))
+		 
+		 (proof-save-with-hole-regexp
+		  (list proof-save-with-hole-regexp save-discrim))))))
+
+	   (if proof-script-next-entity-regexps
+	       ;; Enable func-menu for this mode if regexps set
+	       (progn
+		 (pushnew
+		  (cons major-mode 'proof-script-next-entity-regexps)
+		  fume-function-name-regexp-alist)
+		 (pushnew
+		  (cons major-mode proof-script-find-next-entity-fn)
+		  fume-find-function-name-method-alist)))))
+
+  ;; FIXME da: does proof mode hook call belong here? 
   (run-hooks 'proof-mode-hook))
 
 
-
 (provide 'proof-script)
 ;; proof-script.el ends here.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7354d3df..a42de00d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1011,7 +1011,7 @@ Annotations are characters 128-255."
 (easy-menu-define proof-shell-mode-menu
 		  proof-shell-mode-map
 		  "Menu used in Proof General shell mode."
-		  (cons proof-mode-name (cdr proof-shell-menu)))
+		  (cons proof-general-name (cdr proof-shell-menu)))
 
 
 
@@ -1070,13 +1070,13 @@ Annotations are characters 128-255."
 
 (eval-and-compile
 (define-derived-mode proof-universal-keys-only-mode fundamental-mode
-    proof-mode-name "Universal keymaps only"
+    proof-general-name "Universal keymaps only"
     (suppress-keymap proof-universal-keys-only-mode-map 'all)
     (proof-define-keys proof-universal-keys-only-mode-map proof-universal-keys)))
 
 (eval-and-compile			; to define vars
 (define-derived-mode pbp-mode proof-universal-keys-only-mode
-  proof-mode-name "Proof by Pointing"
+  proof-general-name "Proof by Pointing"
   ;; defined-derived-mode pbp-mode initialises pbp-mode-map
   (setq proof-buffer-type 'pbp)
   ;; (define-key pbp-mode-map [(button2)] 'pbp-button-action)
@@ -1092,16 +1092,9 @@ Annotations are characters 128-255."
 (easy-menu-define proof-response-mode-menu
 		  proof-response-mode-map
 		  "Menu for Proof General response buffer."
-		  (cons proof-mode-name
+		  (cons proof-general-name
 			(cdr proof-shared-menu)))
 
 
-			
-
-
-
-
-
-
 (provide 'proof-shell)
 ;; proof-shell.el ends here.
\ No newline at end of file
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index d4bfb137..1181b5be 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -17,6 +17,32 @@
   expression matching any of its elements"
   (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|"))
 
+(defun proof-regexp-alt (&rest args)
+  "Return the regexp which matches any of the regexps ARGS."
+  ;; Is this not available in some library?
+  (let ((res ""))
+    (dolist (regexp args res)
+      (setq res (concat res (if (string-equal res "") "\\(" "\\|\\(")
+			regexp "\\)")))))
+
+(defun proof-regexp-region (start end)
+  "Return regexp matching START anything over several lines END."
+  ;; FIXME: would like to use shy grouping here \\(?: but it seems
+  ;; buggy or unimplemented in XEmacs.
+  ;; WARNING: this produces nasty regexps that lead to stack
+  ;; overflows.  It's better to have a loop that searches over lines,
+  ;; see next function.
+  (concat "\\(" start "\\)\\(\n\\|.\\)*\\(" end "\\)"))
+
+(defun proof-re-search-forward-region (startre endre)
+  "Search for a region delimited by regexps STARTRE and ENDRE.
+Return the start position of the match for STARTRE, or
+nil if a region cannot be found."
+  (if (re-search-forward startre nil t)
+      (let ((start (match-beginning 0)))
+	(if (re-search-forward endre nil t)
+	    start))))
+
 ;; Generic font-lock
 
 ;; proof-commands-regexp is used for indentation