diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-09-21 10:42:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-09-21 10:42:12 +0000 |
| commit | a807174a176715da829648fae7319c46113c4048 (patch) | |
| tree | 919eb61f1cd8f1c3d589a37d3714ca6316e230db /generic/pg-user.el | |
| parent | 821a5f41ca6e9715337a3176d6a82e4da6643ae1 (diff) | |
proof-autosend-loop: adjust to only update modified tick when sending
(engages autosend slightly more often, but not quite often enough)
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 215009c4..cfc1e1fc 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1425,7 +1425,10 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." (proof-with-current-buffer-if-exists proof-script-buffer (unless (or (proof-locked-region-full-p) proof-shell-busy - (eq (buffer-chars-modified-tick) proof-autosend-modified-tick)) + ;; TODO: re-engage autosend after C-c C-n even if not modified. + (eq (buffer-chars-modified-tick) proof-autosend-modified-tick) + (and proof-autosend-all + (eq proof-shell-last-queuemode 'retracting))) (setq proof-autosend-running t) (setq proof-autosend-modified-tick (buffer-chars-modified-tick)) (if proof-autosend-all @@ -1435,29 +1438,27 @@ assuming the undo-in-region behavior will apply if ARG is non-nil." (defun proof-autosend-loop-all () "Send commands from the script until an error, complete, or input appears." - (unless (eq proof-shell-last-queuemode 'retracting) - (message "Sending commands to prover...") - (setq proof-autosend-modified-tick (buffer-chars-modified-tick)) - (unwind-protect - (progn - (save-excursion - (goto-char (point-max)) - (proof-assert-until-point - (if proof-multiple-frames-enable - 'no-minibuffer-messages ; nb: not API + (message "Sending commands to prover...") + (unwind-protect + (progn + (save-excursion + (goto-char (point-max)) + (proof-assert-until-point + (if proof-multiple-frames-enable + 'no-minibuffer-messages ; nb: not API '(no-response-display no-error-display no-goals-display)))) - (proof-shell-wait t) ; interruptible - (cond - ((eq proof-shell-last-output-kind 'error) - (message "Sending commands to prover...error")) - ((and (input-pending-p) proof-shell-busy) - (proof-interrupt-process) - (message "Sending commands to prover...interrupted") - (proof-shell-wait)) - (t - (message "Sending commands to prover...done"))))))) + (proof-shell-wait t) ; interruptible + (cond + ((eq proof-shell-last-output-kind 'error) + (message "Sending commands to prover...error")) + ((and (input-pending-p) proof-shell-busy) + (proof-interrupt-process) + (message "Sending commands to prover...interrupted") + (proof-shell-wait)) + (t + (message "Sending commands to prover...done")))))) (defun proof-autosend-loop-next () "Send the next command from the script and indicate its success/otherwise." |