Fixed up proof-shell-proof-completed mess nicely.

2 files changed, 69 insertions, 81 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4f0aeafd..707c0477 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1343,11 +1343,14 @@ It is safe to leave this variable unset (as nil)."
 
 (defcustom proof-shell-proof-completed-regexp nil
   "Regexp matching output indicating a finished proof.
-Match number 1 should be the response text.
 
-This is used to enable the QED function (save a proof) and
-to control what output appears in the response buffer at the
-end of a proof."
+When output which matches this regexp is seen, we clear the goals
+buffer in case this is not also marked up as a `goals' type of
+message.
+
+We also enable the QED function (save a proof) and will automatically
+close off the proof region if another goal appears before a save
+command."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
@@ -1711,23 +1714,6 @@ for parsing the is disabled."
   :type 'character
   :group 'proof-goals)
 
-;; FIXME: remove this setting for 3.2, by matching on
-;; completed-regexp as an extra step, after errors/interrupt,
-;; but as well as ordinary output.
-(defcustom proof-goals-display-qed-message nil
-  "If non-nil, display the proof-completed message in the goals buffer.
-For some proof assistants (e.g. Isabelle) it seems aesthetic to
-display the QED message in the goals buffer, even though it doesn't
-contain any goals and shouldn't be marked up for proof-by-pointing.
-
-If this setting is non-nil, QED messages appear in the goals
-buffer.  Otherwise they appear in the response buffer.
-
-This is a hack specially for Isabelle.  DON'T USE IT.
-It will be removed in a future version of Proof General."
-  :type 'boolean
-  :group 'proof-goals)
-
 (defcustom proof-goals-font-lock-keywords nil
   "Value of font-lock-keywords used to fontify the goals output.
 NB: the goals output is not kept in font-lock-mode because the
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 78986fc7..5814172e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -887,6 +887,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook."
   "Like string-match except returns nil if REGEXP is nil."
   (and regexp (string-match regexp string)))
 
+      
 (defun proof-shell-process-output (cmd string)
   "Process shell output (resulting from CMD) by matching on STRING.
 CMD is the first part of the proof-action-list that lead to this
@@ -920,67 +921,68 @@ This function can return one of 4 things as the symbol: 'error,
 'interrupt, 'loopback, or nil. 'loopback means this was output from
 pbp, and should be inserted into the script buffer and sent back to
 the proof assistant."
-  (cond
-   ((proof-shell-string-match-safe proof-shell-interrupt-regexp string)
-    'interrupt)
-
-     ((proof-shell-string-match-safe proof-shell-error-regexp string)
-      (cons 'error (proof-shell-strip-special-annotations
-		    (substring string
-			       (match-beginning 0)))))
-	 
-   ((proof-shell-string-match-safe proof-shell-abort-goal-regexp string)
-    (proof-clean-buffer proof-goals-buffer)
-    (setq proof-shell-delayed-output (cons 'insert "\nAborted\n"))
-    ())
-
-   ;; FIXME: remove proof-goals-display-qed-message setting in version 3.2,
-   ;; by matching on completed-regexp as an extra step again when a goal
-   ;; is found, or alternatively in same part as errors/interrupt
-   ;; (but that risks displaying no subgoals message twice in Isabelle!).
-   ;; We can also remove the match-string 1 mess too, modify every
-   ;; instance accordingly.
-   ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string)
-    (proof-clean-buffer proof-goals-buffer)
-    (setq proof-shell-proof-completed 0) ; counts commands since proof complete.
-    (setq proof-shell-delayed-output
-	  (cons (if proof-goals-display-qed-message
-		    'analyse 'insert)
-		(match-string 1 string))))
-
-   ((proof-shell-string-match-safe proof-shell-start-goals-regexp string)
-    (let ((start (match-end 0))
-	  end)
-      ;; Find the last goal string in the output
-      (while (string-match proof-shell-start-goals-regexp string start)
-	(setq start (match-end 0)))
-      ;; Ugly hack: provers with special characters don't include
-      ;; the match in their goals output.  Others do.
-      (unless proof-shell-first-special-char
-	(setq start (match-beginning 0)))
-      (setq end (if proof-shell-end-goals-regexp
-		    (string-match proof-shell-end-goals-regexp string start)
-		  (length string)))
-      (setq proof-shell-delayed-output 
-	    (cons 'analyse (substring string start end)))))
-       
+  (or
+   ;; First check for error, interrupt, abort, proof completed
+   (cond
+    ((proof-shell-string-match-safe proof-shell-interrupt-regexp string)
+     'interrupt)
+    
+    ((proof-shell-string-match-safe proof-shell-error-regexp string)
+     (cons 'error (proof-shell-strip-special-annotations
+		   (substring string
+			      (match-beginning 0)))))
+    
+    ((proof-shell-string-match-safe proof-shell-abort-goal-regexp string)
+     (proof-clean-buffer proof-goals-buffer)
+     (setq proof-shell-delayed-output (cons 'insert "\nAborted\n"))
+     ())
+    
+    ((proof-shell-string-match-safe proof-shell-proof-completed-regexp string)
+     ;; In case no goals display
+     (proof-clean-buffer proof-goals-buffer)
+     ;; counter of commands since proof complete.
+     (setq proof-shell-proof-completed 0) 
+     ;; But!  We carry on matching below for goals output, so that
+     ;; provers may include proof completed message as part of 
+     ;; goals message (Isabelle, HOL) or not (LEGO, Coq).
+     nil))
+
+   ;; Check for remaining things
+   (cond
+    ((proof-shell-string-match-safe proof-shell-start-goals-regexp string)
+     (let ((start (match-end 0))
+	   end)
+       ;; Find the last goal string in the output
+       (while (string-match proof-shell-start-goals-regexp string start)
+	 (setq start (match-end 0)))
+       ;; Ugly hack: provers with special characters don't include
+       ;; the match in their goals output.  Others do.
+       (unless proof-shell-first-special-char
+	 (setq start (match-beginning 0)))
+       (setq end (if proof-shell-end-goals-regexp
+		     (string-match proof-shell-end-goals-regexp string start)
+		   (length string)))
+       (setq proof-shell-delayed-output 
+	     (cons 'analyse (substring string start end)))))
+    
     ;; Test for a proof by pointing command hint
-     ((proof-shell-string-match-safe proof-shell-result-start string)
-      (let (start end)
-	(setq start (+ 1 (match-end 0)))
-	(string-match proof-shell-result-end string)
-	(setq end (- (match-beginning 0) 1))
-	(cons 'loopback (substring string start end))))
-   
-     ;; Hook to tailor proof-shell-process-output to a specific proof
-     ;; system, in the case that all the above matches fail.
-   ((and proof-shell-process-output-system-specific
-	 (funcall (car proof-shell-process-output-system-specific)
-		  cmd string))
-    (funcall (cdr proof-shell-process-output-system-specific)
-	     cmd string))
-
-   (t (setq proof-shell-delayed-output (cons 'insert string)))))
+    ((proof-shell-string-match-safe proof-shell-result-start string)
+     (let (start end)
+       (setq start (+ 1 (match-end 0)))
+       (string-match proof-shell-result-end string)
+       (setq end (- (match-beginning 0) 1))
+       (cons 'loopback (substring string start end))))
+    
+    ;; Hook to tailor proof-shell-process-output to a specific proof
+    ;; system, in the case that all the above matches fail.
+    ((and proof-shell-process-output-system-specific
+	  (funcall (car proof-shell-process-output-system-specific)
+		   cmd string))
+     (funcall (cdr proof-shell-process-output-system-specific)
+	      cmd string))
+
+    ;; Finally, any other output will appear as a response.
+    (t (setq proof-shell-delayed-output (cons 'insert string))))))
 
 
 ;;