4 files changed, 26 insertions, 12 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 4adc3c39..1a61a192 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1435,9 +1435,9 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 (defun proof-autosend-loop ()
   (proof-with-current-buffer-if-exists proof-script-buffer
     (unless (proof-locked-region-full-p)
-	(proof-autosend-loop1))))
+	(proof-autosend-loop-all))))
 
-(defun proof-autosend-loop1 ()
+(defun proof-autosend-loop-all ()
   "Send commands from the script until an error, complete, or input appears."
   (when proof-autosend-error-point
     (if (< proof-last-edited-low-watermark proof-autosend-error-point)
@@ -1445,7 +1445,8 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 	;; FIXME: this isn't good enough, edit of the command which caused
 	;; the error, or earlier is what we want.  Need to record that.
 	(setq proof-autosend-error-point nil)))
-  (unless proof-autosend-error-point 
+  (unless (or proof-autosend-error-point  
+	      (eq proof-shell-last-queuemode 'retracting))
     (message "Sending commands to prover...")
     (setq proof-autosend-running t)
     (unwind-protect
@@ -1471,6 +1472,10 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 	    (message "Sending commands to prover...done."))))
       (setq proof-autosend-running nil))))
 
+;; TODO (see beyondsm)
+;; (defun proof-autosend-loop-next ()
+;;  "Send the next command from the script and indicate its success/otherwise"
+
 
 (provide 'pg-user)
 
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 1bf31ffa..e86fde61 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -83,7 +83,15 @@ has been set.")
 (defvar proof-shell-busy nil
   "A lock indicating that the proof shell is processing.
 When this is non-nil, `proof-shell-ready-prover' will give
-an error.")
+an error.
+
+When processing commands from a buffer for script management,
+this will be set to either 'advancing or 'retracting to indicate
+the direction of movement.")
+
+(defvar proof-shell-last-queuemode nil
+  "Flag indicating last direction of proof queue.
+This is actually the last non-nil value of `proof-shell-busy'.")
 
 (defvar proof-included-files-list nil
   "List of files currently included in proof process.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index cc1bce92..8dbf2d14 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2130,7 +2130,8 @@ up to the end of the locked region."
 			      (funcall proof-find-and-forget-fn target)
 			      delete-region))))
 
-    (proof-start-queue (min start end) (proof-unprocessed-begin) actions)))
+    (proof-start-queue (min start end) (proof-unprocessed-begin) 
+		       actions 'retracting)))
 
 ;; FIXME da:  I would rather that this function moved point to
 ;; the start of the region retracted?
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7b4c30ec..1978927f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -176,15 +176,14 @@ No error messages.  Useful as menu or toolbar enabler."
 Runs `proof-state-change-hook' to notify state change.
 If QUEUEMODE is supplied, set the lock to that value."
   (proof-shell-ready-prover queuemode)
-  (setq proof-shell-interrupt-pending nil)
-  (setq proof-shell-busy (or queuemode t))
+  (setq proof-shell-interrupt-pending nil
+	proof-shell-busy (or queuemode t)
+	proof-shell-last-queuemode proof-shell-busy)
   (run-hooks 'proof-state-change-hook))
 
 (defun proof-release-lock ()
   "Release the proof shell lock.  Clear `proof-shell-busy'."
-  (setq proof-shell-busy nil)
-  ;; PG4.0: TODO: alter modeline indicator
-  )
+  (setq proof-shell-busy nil))
 
 
 
@@ -489,6 +488,7 @@ shell buffer, alled by `proof-shell-bail-out' if process exits."
   (setq proof-action-list nil
 	proof-included-files-list nil
 	proof-shell-busy nil
+	proof-shell-last-queuemode nil
 	proof-shell-proof-completed nil
 	proof-nesting-depth 0
 	proof-shell-silent nil
@@ -957,7 +957,7 @@ being processed."
 
 
 ;;;###autoload
-(defun proof-start-queue (start end queueitems)
+(defun proof-start-queue (start end queueitems &optional queuemode)
   "Begin processing a queue of commands in QUEUEITEMS.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
@@ -965,7 +965,7 @@ active scripting buffer for the queue region.
 This function calls `proof-add-to-queue'."
   (if start
       (proof-set-queue-endpoints start end))
-  (proof-add-to-queue queueitems))
+  (proof-add-to-queue queueitems queuemode))
 
 ;;;###autoload
 (defun proof-extend-queue (end queueitems)