diff options
| author | David Aspinall | 2004-04-02 16:45:58 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-04-02 16:45:58 +0000 |
| commit | f4f8a304d04b850d4b265c1fb0b2765ceedf8cc4 (patch) | |
| tree | 2ef6c5663eb8be13efe37ca2c2cd45b650c204c3 /generic | |
| parent | c98ae8dae09def0967426dc6def6252ea455993c (diff) | |
Use proof-shell-wait; comments.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files 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? |