diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 16:53:21 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 16:53:21 +0000 |
| commit | f6ce7d245c88c5892facc40e6461e5a2b4a4ee06 (patch) | |
| tree | f6f8f7ea5e81f751bb4ec16f35f922a60a28e48b /generic/proof-shell.el | |
| parent | 554193ec72d817eda4dd59681927554d0a7cc5ae (diff) | |
Remove redisplay from wait loop, only redisplay on exit. Big speed-up
but doesn't reflect changes as they happen.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f043a7b7..3cf016f0 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1594,19 +1594,21 @@ Only works when system timer has microsecond count available." ;;;###autoload (defun proof-shell-wait (&optional interrupt-on-input) - "Busy wait for `proof-shell-busy' to become nil. + "Busy wait for `proof-shell-busy' to become nil, reading from prover. Needed between sequences of commands to maintain synchronization, because Proof General does not allow for the action list to be extended -in some cases. May be called by `proof-shell-invisible-command'." +in some cases. Also is considerably faster than leaving the Emacs +top-level command loop to read from the prover. +May be called by `proof-shell-invisible-command'." (let ((proverproc (get-buffer-process proof-shell-buffer))) (when proverproc (while (and proof-shell-busy (not quit-flag) (not (and interrupt-on-input (input-pending-p)))) ;; FIXME: check below OK on GE 22/23.1. See Trac #324 - (accept-process-output proverproc 0.01 nil 1) - (redisplay)) + (accept-process-output proverproc 0.01 nil 1)) + (redisplay) (if quit-flag - (error "Proof General: Quit in proof-shell-wait"))))) + (error "Proof General: quit in proof-shell-wait"))))) (defun proof-done-invisible (span) "Callback for proof-shell-invisible-command. |