From f4f8a304d04b850d4b265c1fb0b2765ceedf8cc4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 2 Apr 2004 16:45:58 +0000
Subject: Use proof-shell-wait; comments.

---
 generic/proof-script.el | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 91cd6d43..7ee34569 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -930,8 +930,7 @@ an error is signalled here."
 	    (with-current-buffer buf
 	      (message "%s buffer %s..." name buf)
 	      (funcall fn)
-	      (while proof-shell-busy ; busy wait
-		(sit-for 1))
+	      (proof-shell-wait) ; busy wait
 	      (message "%s buffer %s...done." name buf)
 	      (sit-for 0))
 	  ;; Test to see if action was successful
@@ -2653,7 +2652,7 @@ with something different."
 (defconst proof-script-important-settings
   '(proof-script-comment-start			;
     proof-script-comment-end
-    proof-save-command-regexp
+    proof-save-command-regexp		; [actually, some provers may not have save command]
 ;    proof-goal-command-regexp	        ; not needed if proof-goal-command-p is set
 ;    proof-goal-with-hole-regexp		; non-essential?
 ;    proof-save-with-hole-regexp		; non-essential?
-- 
cgit v1.2.3