From f6ce7d245c88c5892facc40e6461e5a2b4a4ee06 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 18 Aug 2010 16:53:21 +0000
Subject: Remove redisplay from wait loop, only redisplay on exit.  Big
 speed-up but doesn't reflect changes as they happen.

---
 generic/proof-shell.el | 12 +++++++-----
 1 file 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.
-- 
cgit v1.2.3