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

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

9 files changed, 278 insertions, 111 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 4a4ddc0c..5a4998fd 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -430,7 +430,6 @@
 	proof-kill-goal-command coq-kill-goal-command)
 
   (setq proof-goal-command-p 'coq-goal-command-p
-	proof-nested-goals-allowed t
 	proof-count-undos-fn 'coq-count-undos
 	proof-find-and-forget-fn 'coq-find-and-forget
         proof-goal-hyp-fn 'coq-goal-hyp
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index a757197a..a9499495 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2867,7 +2867,54 @@ This variable may not need to be set: a default value which should
 work for goal..saves is calculated from @code{proof-goal-with-hole-regexp},
 @code{proof-goal-command-regexp}, and @code{proof-save-with-hole-regexp}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: nilproof-goal-command-p nil 
+
+@c TEXI DOCSTRING MAGIC: proof-script-find-next-entity-fn
+@defvar proof-script-find-next-entity-fn 
+Name of function to find next interesting entity in a script buffer.@*
+This is used to configure @code{func-menu}.  The default value is
+@code{proof-script-find-next-entity}, which searches for the next entity
+based on @code{fume-function-name-regexp} which by default is set from
+@code{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.
+
+Note that @code{proof-script-next-entity-regexps} is set to a default value
+from @code{proof-goal-with-hole-regexp} and @code{proof-save-with-hole-regexp} in
+the function @code{proof-config-done}, so you may not need to worry about any
+of this.  See whether function menu does something sensible by
+default.
+@end defvar
+
+@c TEXI DOCSTRING MAGIC: proof-goal-command-p 
+
+@c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour
+@defvar proof-completed-proof-behaviour 
+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
+@lisp
+"save" command appears --- or it may not appear at all.  Unless
+@end lisp
+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:
+@lisp
+        nil  -  nothing special; close only when a save arrives
+  @code{'closeany}  -  close as soon as the next command arrives, save or not
+ @code{'closegoal}  -  close when the next "goal" command arrives
+    @code{'extend}  -  keep extending the closed region until a save or goal.
+@end lisp
+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 @code{proof-lift-global} mechanism.  Of course, this is risky because of
+nested contexts!
+@end defvar
+ 
 @c TEXI DOCSTRING MAGIC: proof-lift-global
 @defvar proof-lift-global 
 Function which lifts local lemmas from inside goals out to top level.@*
@@ -3871,7 +3918,9 @@ read.
 
 @c TEXI DOCSTRING MAGIC: proof-shell-proof-completed
 @defvar proof-shell-proof-completed 
-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 is actually the number of commands that have
+been processed since the proof was completed.
 @end defvar
 
 The @file{proof.el} also loads @file{proof-config.el} which declares the
@@ -4272,11 +4321,11 @@ Process the @code{proof-action-list}.
 
 If this function is called with a non-empty @code{proof-action-list}, the
 head of the list is the previously executed command which succeeded.
-We execute (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on
-any following items which have @code{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 (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on any
+following items which have @code{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.
 @end defun
@@ -4337,22 +4386,36 @@ the last urgent message seen.
 @defun proof-shell-process-output cmd string
 Process shell output (resulting from @var{cmd}) by matching on @var{string}.@*
 @var{cmd} is the first part of the @code{proof-action-list} that lead to this
-output.
+output.  The result of this function is a pair (@var{symbol} @var{newstring}).
 
-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 @code{proof-shell-delayed-output} to a cons 
-cell of ('insert . @var{text}) where @var{text} is the text string to 
-be inserted.
+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
+@lisp
+  @code{proof-shell-interrupt-regexp}
+  @code{proof-shell-error-regexp}
+  @code{proof-shell-abort-goal-regexp}
+  @code{proof-shell-proof-completed-regexp}
+  @code{proof-shell-result-start}
+@end lisp
+All other output from the proof engine will be reported to the user in
+the response buffer by setting @code{proof-shell-delayed-output} to a cons
+cell of ('insert . @var{text}) where @var{text} is the text string to be inserted.
 
-To extend this function, set
-@code{proof-shell-process-output-system-specific}.
+Order of testing is: interrupt, abort, error, completion.
 
-This function - it can return one of 4 things: @code{'error}, @code{'interrupt},
-@code{'loopback}, or nil. @code{'loopback} means this was output from pbp, and
-should be inserted into the script buffer and sent back to the proof
-assistant.
+To extend this function, set @code{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
+@code{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: @code{'error},
+@code{'interrupt}, @code{'loopback}, or nil. @code{'loopback} means this was output from
+pbp, and should be inserted into the script buffer and sent back to
+the proof assistant.
 @end defun
 
 @c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker
@@ -4423,6 +4486,9 @@ 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.
+
+After processing the current output, the last step undertaken
+by the filter is to send the next command from the queue.
 @end defun
 
 
diff --git a/etc/lego/unsaved-goals.l b/etc/lego/unsaved-goals.l
index 55275eca..dd9c9646 100644
--- a/etc/lego/unsaved-goals.l
+++ b/etc/lego/unsaved-goals.l
@@ -1,9 +1,34 @@
 (* 
-  test case for closing off unsaved goals:
-  P.G. should close Goal->Immed even though there
-  is no Save.  Pred definition should not be
-  part of closed region  
-  (test with undoing and redoing) 
+  Some test cases for closing off unsaved goals, 
+  and the setting proof-completed-proof-behaviour.
+
+  David Aspinall, November 1999.
+
+  Things work fairly well in lego with 
+
+       proof-completed-proof-behaviour='closeany
+
+  In that case, undoing/redoing later declarations 
+  (E and F) following the completed proof works okay, and
+  in the absence of declarations, things work fine.
+    
+  Declarations in LEGO are global, and forgetting a
+  declaration when a proof is still open (even if complete)
+  aborts the proof!  So a proper handling would need to
+  trigger a *further* retraction when the "Forget D" is
+  issued undoing the definition of D.  Never mind.
+
+  With proof-completed-proof-behaviour='closegoal or 'extend,
+  undoing the first goal doesn't forget the declarations.
+
+  This file even causes internal errors in LEGO!
+
+     Warning: forgetting a finished proof
+
+     LEGO detects unexpected exception named "InfixInternal"
+
+  Test with undoing and redoing, and various settings
+  for proof-completed-proof-behaviour
 *)
    
 
@@ -16,8 +41,14 @@ Refine H;
 intros;
 andI;
 Immed;
-
-[Pred = [s:Type]s->Prop];
+[D = Type];
+[E = Type];
+[F = Type];
 
 Goal {A,B:Prop}(and A B) -> (and B A);
+intros;
+Refine H;
+intros;
+andI;
+Immed;
 
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.
diff --git a/isa/isa.el b/isa/isa.el
index db974ac8..c4d72822 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -145,6 +145,10 @@ and script mode."
    proof-state-preserving-p	'isa-state-preserving-p
    proof-parse-indent		'isa-parse-indent
    proof-stack-to-indent	'isa-stack-to-indent
+
+   ;; close goal..save regions eagerly
+   proof-completed-proof-behaviour 'closeany
+
    proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list
    proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";"
    proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";"))
diff --git a/lego/lego.el b/lego/lego.el
index d3d02c92..981e5e81 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -112,7 +112,8 @@ Activates extended printing routines required for Proof General.")
 (defvar lego-shell-cd "Cd \"%s\""
   "*Command of the inferior process to change the directory.") 
 
-(defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state"
+(defvar lego-shell-abort-goal-regexp 
+  "KillRef: ok, not in proof state\\|Forget forced KillRef"
   "*Regular expression indicating that the proof of the current goal
   has been abandoned.")
 
@@ -358,6 +359,7 @@ Checks the width in the `proof-goals-buffer'"
 	proof-info-command "Help")
 
   (setq proof-goal-command-p 'lego-goal-command-p
+	proof-completed-proof-behaviour 'closeany ; new in 3.0
 	proof-count-undos-fn 'lego-count-undos
 	proof-find-and-forget-fn 'lego-find-and-forget
         proof-goal-hyp-fn 'lego-goal-hyp