diff options
Diffstat (limited to 'generic/pg-user.el')
-rw-r--r-- | generic/pg-user.el | 11 |
1 files changed, 8 insertions, 3 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) |