proof-nested-goals-allowed -> proof-completed-proof-behaviour

Patch for more flexible handling of closing goal...save regions
after proof has been completed.

4 files changed, 147 insertions, 82 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1bae2e5c..cf03c487 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -803,13 +803,28 @@ default."
   :type 'function
   :group 'proof-script)
 
-(defcustom proof-nested-goals-allowed nil
-  "Whether the proof assistant allows nested goals.  
-If it does not, Proof General assumes that successive goals automatically 
-discard the previous proof state  
-
-Some proof assistants may simply give an error when nested goals are
-attempted, so the setting of this variable doesn't matter."
+(defcustom proof-completed-proof-behaviour nil
+  "Indicates how Proof General treats commands beyond the end of a proof.
+Normally goal...save regions are \"closed\", i.e. made atomic for undo.
+But once a proof has been completed, there may be a delay before the
+\"save\" command appears --- or it may not appear at all.  Unless
+nested proofs are supported, this can spoil the undo-behaviour in
+script management since once a new goal arrives the old undo history
+may be lost in the prover.  So we allow Proof General to close 
+off the goal..[save] region in more flexible ways.  
+The possibilities are:
+
+        nil  -  nothing special; close only when a save arrives
+  'closeany  -  close as soon as the next command arrives, save or not
+ 'closegoal  -  close when the next \"goal\" command arrives
+    'extend  -  keep extending the closed region until a save or goal.
+
+If your proof assistant allows nested goals, it will be wrong to close
+off the portion of proof so far, so this variable should be set to nil.
+There is no built-in understanding of the undo behaviour of nested
+proofs; instead there is some support for un-nesting nested proofs in
+the proof-lift-global mechanism.  Of course, this is risky because of
+nested contexts!"
   :type 'boolean
   :group 'proof-script)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index f5a81ca0..22f78511 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -955,8 +955,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
   ;;FIXME tms: needs implementation
   nil)
 
-(defvar proof-previous-proof-completed nil
-  "Copy of proof-shell-proof-completed from previous scripting command.")
+
 
 (defun proof-done-advancing (span)
   "The callback function for assert-until-point."
@@ -977,21 +976,27 @@ the ACS is marked in the current buffer. If CMD does not match any,
     (proof-set-queue-start end)
     (setq cmd (span-property span 'cmd))
     (cond
-     ;; * Comments just get highlighted
+     ;; CASE 1: Comments just get highlighted
      ((eq (span-property span 'type) 'comment)
       (set-span-property span 'mouse-face 'highlight))
      
-     ;; "ACS" for future implementation
-     ;; ((proof-check-atomic-sequents-lists span cmd end))
-
-     ;; * Save command seen, now we'll amalgamate spans.
+     ;; CASE 2: Save command seen, now we'll amalgamate spans.
      ((and (proof-string-match proof-save-command-regexp cmd)
 	    (funcall proof-really-save-command-p span cmd))
 
+      (unless (eq proof-shell-proof-completed 1)
+	;; We expect saves to succeed only for recently completed proofs.
+	;; Give a hint to the proof assistant implementor in case something
+	;; odd is going on.
+	(proof-debug 
+	 (format
+	  "Proof General note: save command with proof-shell-proof-completed=%s"
+	  proof-shell-proof-completed)))
+
+      (setq proof-shell-proof-completed nil)
+
+      ;; FIXME: subroutine here:
       (let (nam gspan next)
-	;; First, clear the proof completed flag
-	(setq proof-shell-proof-completed nil)
-	(setq proof-previous-proof-completed nil)
 
 	;; Try to set the name of the theorem from the save
 	(and proof-save-with-hole-regexp
@@ -1020,9 +1025,11 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	       (proof-string-match proof-goal-with-hole-regexp
 				   (span-property gspan 'cmd))
 	       (setq nam (match-string 2 (span-property gspan 'cmd)))))
-	;; As a final desparate attempt, set the name to 
-	;; proof-unnamed-theorem-name  (Coq actually uses a default
-	;; name for unnamed theorems, believe it or not).
+
+	;; As a final desparate attempt, set the name to
+	;; proof-unnamed-theorem-name (Coq actually uses a default
+	;; name for unnamed theorems, believe it or not, and issues
+	;; a name-binding error for two unnamed theorems in a row!).
 	(unless nam
 	  (setq nam proof-unnamed-theorem-name))
 
@@ -1039,27 +1046,40 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	(and proof-lift-global
 	     (funcall proof-lift-global gspan)))))
 
-     ;; NEW CASE:
-     ;; Proof completed in *previous* command, no nested goals
-     ;; allowed.  We make a fake goal-save from any previous 
-     ;; goal to the command before the present one.
-
-
-
-     ;; * Goal command just processed, no nested goals allowed.
+     ;; CASE 3: Proof completed one step or more ago, non-save
+     ;; command seen, no nested goals allowed.
+     ;; 
      ;; We make a fake goal-save from any previous 
      ;; goal to the command before the present one.
-     ;; (This is a hack for Isabelle and LEGO to allow smooth
-     ;; undoing in proofs which have no "qed" statements).
+     ;;
+     ;; This is a hack to allow smooth undoing in proofs which have no
+     ;; "qed" statements.  If your proof assistant doesn't allow
+     ;; these "unclosed" proofs, then you can safely set
+     ;; proof-completed-proof-behaviour.
+     ;;
      ;; FIXME: abstract common part of this case and case above,
      ;; to improve code by making a useful subroutine.
-     ((and (not proof-nested-goals-allowed)
-	   (funcall proof-goal-command-p cmd))
-      (let (nam gspan hitsave dels)
-	;; A preliminary search backwards to 
-	;; see if we can find a previous goal before
-	;; a save or the start of the buffer.
-	(setq gspan (prev-span span 'type))
+     ((and
+       proof-shell-proof-completed
+       (or (and (eq proof-completed-proof-behaviour 'extend)
+		(>= proof-shell-proof-completed 0))
+	   (and (eq proof-completed-proof-behaviour 'closeany)
+		(> proof-shell-proof-completed 0))
+	   (and (eq proof-completed-proof-behaviour 'closegoal)
+		(funcall proof-goal-command-p cmd))))
+
+      (if (eq proof-completed-proof-behaviour 'extend)
+	  ;; In the extend case, the context of the proof grows
+	  ;; until we hit a save or new goal.
+	  (incf proof-shell-proof-completed)
+	(setq proof-shell-proof-completed nil))
+
+      (let* ((swallow  (eq proof-completed-proof-behaviour 'extend))
+	     (gspan    (if swallow span (prev-span span 'type)))
+	     (newend   (if swallow (span-end span) (span-start span)))
+	    nam hitsave dels)
+	;; Search backwards to see if we can find a previous goal
+	;; before a save or the start of the buffer.
 	(while 
 	    (and 
 	     gspan
@@ -1074,15 +1094,17 @@ the ACS is marked in the current buffer. If CMD does not match any,
 		     (setq hitsave t))))))
 	  (setq dels (cons gspan dels))
 	  (setq gspan (prev-span gspan 'type)))
-	(unless (or hitsave (null gspan))
+	(if (or hitsave (null gspan))
+	    (proof-debug
+     "Proof General strangeness: unclosed proof completed, but couldn't find its start!")
 	  ;; If we haven't hit a save or the start of the buffer,
 	  ;; we make a fake goal-save region.
 
-	  ;; Delete spans between the previous goal and new goal
+	  ;; Delete spans between the previous goal and new command
 	  (mapcar 'delete-span dels)
 
 	  ;; Try to set a name from the goal
-	  ;; (useless for Isabelle)
+	  ;; (useless for provers like Isabelle)
 	  (and proof-goal-with-hole-regexp
 	       (proof-string-match proof-goal-with-hole-regexp
 				   (span-property gspan 'cmd))
@@ -1091,18 +1113,25 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	  (unless nam
 	    (setq nam proof-unnamed-theorem-name))
 	  
-	  ;; Now make the new goal-save span
-	  (set-span-end gspan (span-start span))
+	  ;; Now make the new or extended goal-save span
+	  ;; Don't bother with Coq's lift global stuff, we assume this
+	  ;; case is only good for non-nested goals.
+	  (set-span-end gspan newend)
 	  (set-span-property gspan 'mouse-face 'highlight)
 	  (set-span-property gspan 'type 'goalsave)
-	  (set-span-property gspan 'name nam)))
-	;; Finally, do the usual thing with highlighting.
-	;; Don't bother with Coq's lift global stuff, we assume
-	;; this code is only good for non-nested goals.
-	(set-span-property span 'mouse-face 'highlight))
-     ;; 
-     ;; Otherwise, some other kind of command (or a nested goal).
+	  (set-span-property gspan 'name nam))
+	;; Finally, do the usual thing with highlighting for the span.
+	(unless swallow
+	  (set-span-property span 'mouse-face 'highlight))))
+
+
+     ;; "ACS" for possible future implementation
+     ;; ((proof-check-atomic-sequents-lists span cmd end))
+
+     ;; CASE 4:  Some other kind of command (or a nested goal).
      (t
+      (if proof-shell-proof-completed
+	  (incf proof-shell-proof-completed))
       (set-span-property span 'mouse-face 'highlight)
       (and proof-global-p 
 	   (funcall proof-global-p cmd)
@@ -1444,12 +1473,14 @@ appropriate."
 
 
 (defun proof-done-retracting (span)
-  "Update display after proof process has reset its state.
+  "Callback for proof-retract-until-point.
+We update display after proof process has reset its state.
 See also the documentation for `proof-retract-until-point'.
-Optionally delete the region corresponding to the proof sequence."
-  ;; 10.9.99: da: added this line so that undo always clears the
-  ;; proof completed flag.  Rationale is that undoing never leaves
-  ;; prover in a "proof just completed" state.
+Optionally delete the region corresponding to the proof sequence.
+After an undo, we clear the proof completed flag.  The rationale
+is that undoing never leaves prover in a \"proof just completed\" 
+state, which is true for some proof assistants (but probably not
+others)."
   (setq proof-shell-proof-completed nil)
   (if (span-live-p span)
       (let ((start (span-start span))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 0a244b1c..6fb67920 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1002,22 +1002,36 @@ Then we call `proof-shell-handle-error-hook'. "
 (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
-output.
-
-This function deals with errors, start of proofs, abortions of
-proofs and completions of proofs.  All other output from the proof
-engine is simply reported to the user in the response buffer
-by setting proof-shell-delayed-output to a cons 
-cell of ('insert . TEXT) where TEXT is the text string to 
-be inserted.
-
-To extend this function, set
-proof-shell-process-output-system-specific.
-
-This function - it can return one of 4 things: '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."
+output.  The result of this function is a pair (SYMBOL NEWSTRING).
+
+Here is where we recognizes interrupts, abortions of proofs, errors,
+completions of proofs, and proof step hints (proof by pointing results).
+They are checked for in this order, using
+ 
+  proof-shell-interrupt-regexp
+  proof-shell-error-regexp
+  proof-shell-abort-goal-regexp
+  proof-shell-proof-completed-regexp
+  proof-shell-result-start
+
+All other output from the proof engine will be reported to the user in
+the response buffer by setting proof-shell-delayed-output to a cons
+cell of ('insert . TEXT) where TEXT is the text string to be inserted.
+
+Order of testing is: interrupt, abort, error, completion.
+
+To extend this function, set proof-shell-process-output-system-specific.
+
+The \"aborted\" case is intended for killing off an open proof during
+retraction.  Typically it the error message caused by a
+proof-kill-goal-command.  It simply inserts the word \"Aborted\" into
+the response buffer.  So it is expected to be the result of a 
+retraction, rather than the indication that one should be made.
+
+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)
@@ -1026,22 +1040,22 @@ assistant."
     (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)
     (proof-clean-buffer proof-goals-buffer)
-    (setq proof-shell-proof-completed t)
+    (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)
-    (setq proof-shell-proof-completed nil)
+;    (setq proof-shell-proof-completed nil)
     (let (start end)
       (while (progn (setq start (match-end 0))
 		    (string-match proof-shell-start-goals-regexp 
@@ -1051,7 +1065,7 @@ assistant."
 	    (cons 'analyse (substring string start end)))))
        
    ((proof-shell-string-match-safe proof-shell-result-start string)
-    (setq proof-shell-proof-completed nil)
+;    (setq proof-shell-proof-completed nil)
     (let (start end)
       (setq start (+ 1 (match-end 0)))
       (string-match proof-shell-result-end string)
@@ -1213,11 +1227,11 @@ The queue mode is set to 'advancing"
 
 If this function is called with a non-empty proof-action-list, the
 head of the list is the previously executed command which succeeded.
-We execute (ACTION SPAN) on the first item, then (ACTION SPAN) on
-any following items which have proof-no-command as their cmd
-components.  If a there is a next command, send it to the process.
-If the action list becomes empty, unlock the process and remove the
-queue region. 
+We execute (ACTION SPAN) on the first item, then (ACTION SPAN) on any
+following items which have proof-no-command as their cmd components.
+If a there is a next command after that, send it to the process.  If
+the action list becomes empty, unlock the process and remove the queue
+region.
 
 The return value is non-nil if the action list is now empty."
   (or (not proof-action-list)		; exit immediately if finished.
@@ -1595,7 +1609,10 @@ proof-shell-process-output returns: maybe handle an interrupt, an
 error, or deal with ordinary output which is a candidate for the goal
 or response buffer.  Ordinary output is only displayed when the proof
 action list becomes empty, to avoid a confusing rapidly changing
-output."
+output.
+
+After processing the current output, the last step undertaken
+by the filter is to send the next command from the queue."
   (let (cmd res)
     (setq cmd (nth 1 (car proof-action-list)))
     (save-excursion		;current-buffer
diff --git a/generic/proof.el b/generic/proof.el
index dd18ce2a..741e4a01 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -133,7 +133,9 @@ read.")
   "The response buffer.")
 
 (defvar proof-shell-proof-completed nil
-  "Flag indicating that a completed proof has just been observed.")
+  "Flag indicating that a completed proof has just been observed.
+If non-nil, the value counts the commands from the last command
+of the proof (starting from 1).")
 
 ;; FIXME da: remove proof-terminal-string.  At the moment some
 ;; commands need to have the terminal string, some don't.