Added proof-retract-buffer symmetric to proof-process-buffer.

Added question to user when switching scripting buffer,
and new option proof-auto-retract-other-buffers to disable question.
This reimplements the old "steal scripting?" idea.

3 files changed, 42 insertions, 6 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 72c6d3cc..6b370382 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -137,10 +137,27 @@ With this option active, the locked region will automatically be
 unlocked when the user attempts to edit it.   To make use of this
 option, proof-strict-read-only should be turned off.
 
-Note: this feature has not been implemented yet, it's only an idea."
+Note: this feature has not been implemented yet, it is only an idea."
   :type 'boolean
   :group 'proof-general)
 
+(defcustom proof-auto-retract-other-buffers
+  nil
+  "*If non-nil, retract automatically when switching scripting buffer.
+With this option active, when scripting is activated in a new
+buffer with an old one partly processed, the old buffer will be
+retracted automatically.  
+
+With this option inactive, the user is questioned instead.
+
+Proof General insists that only one script buffer can be partly 
+processed: all others have to be completely processed or
+completely unprocessed.  This is to make sure that handling of
+multiple files makes sense withing the proof assistant."
+  :type 'boolean
+  :group 'proof-general)
+
+
 (defcustom proof-script-indent nil
   ;; Particular proof assistants can enable this if they feel
   ;; confident about it.  (I don't). -da
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 231368cb..3f9e2622 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -434,13 +434,27 @@ buffers."
 	    
 	  ;; We only allow switching of the Scripting buffer if the
 	  ;; locked region is either empty or full for all buffers.
+	  ;; Give the user the chance to retract previous buffer here.
 	  ;; FIXME: ponder alternative of trying to complete rest
 	  ;; of current scripting buffer?  Allowing to switch when
 	  ;; a goal has been completed?
-	  (or (proof-locked-region-empty-p)
+	  (or (proof-locked-region-empty-p) 
 	      (proof-locked-region-full-p)
-	      (error 
-	       "Cannot have more than one active scripting buffer!"))
+	      (if (or
+		   ;; User option to always force retaction
+		   proof-auto-retract-other-buffers
+		   (yes-or-no-p 
+		    (format
+		     "Scripting already active in buffer: %s, retract there? "
+		     proof-script-buffer)))
+		  (progn
+		    ;; FIXME: Maybe want unwind protect here
+		    (proof-retract-buffer)
+		    ;; Test again to see if retracting happened/was successful
+		    (or (proof-locked-region-empty-p)
+			(proof-locked-region-full-p))))
+	      (error "You cannot have more than one active scripting buffer!"))
+
 	    
 	  ;; Mess around a little bit with the included files
 	  ;; list to make sure it behaves as we expect
@@ -1275,6 +1289,12 @@ the proof script."
   (goto-char (point-max))
   (proof-assert-until-point-interactive))
 
+(defun proof-retract-buffer ()
+  "Retract the current buffer and set point at the start of the buffer."
+  (interactive)
+  (goto-char (point-min))
+  (proof-retract-until-point-interactive))
+
 ;; FIXME da: this could do with some tweaking.  Be careful to
 ;; avoid memory leaks.  If a buffer is killed and it's local
 ;; variables are, then so should all the spans which were allocated
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 805c0dfb..60f52fef 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -334,8 +334,7 @@ Move point if the end of the locked position is invisible."
   ;; proof-retract-file might be better here!
   (interactive)
   (proof-toolbar-move
-   (goto-char (point-min))
-   (proof-retract-until-point-interactive))	; gives error if process busy
+   (proof-retract-buffer))	; gives error if process busy
   (proof-toolbar-follow))
 
 ;;