aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-11-08 14:56:58 +0000
committerDavid Aspinall1999-11-08 14:56:58 +0000
commitb2b8286d5b90883c512f864850b19a35b26001c2 (patch)
treee381c3d7de0569f0cc1b3b2d4e2c8645ec5d4587
parent32ebebb0ed73f11aa9dd55ec0859a0e3757253b9 (diff)
Comments.
-rw-r--r--isa/isa.el9
1 files changed, 6 insertions, 3 deletions
diff --git a/isa/isa.el b/isa/isa.el
index d1c17ad6..72ea520f 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -208,15 +208,15 @@ no regular or easily discernable structure."
proof-shell-leave-annotations-in-output t
- ;; === ANNOTATIONS === ones below here are broken
+ ;; === ANNOTATIONS === ones here are broken
proof-shell-result-start "\372 Pbp result \373"
proof-shell-result-end "\372 End Pbp result \373"
proof-analyse-using-stack t
proof-shell-start-char ?\372
proof-shell-end-char ?\373
proof-shell-field-char ?\374
- ;; NEW NEW for multiple files
- ;; === NEW NEW: multiple file stuff. move elsewhere later.
+
+ ;; === MULTIPLE FILE HANDLING ===
proof-shell-process-file
(cons
;; Theory loader output and verbose update() output.
@@ -264,6 +264,9 @@ This is a hook function for proof-activate-scripting-hook."
;; up to date, after all, the user wasn't allowed to edit
;; anything that this file depends on, was she?
(progn
+ ;; Wait after sending, so that queue is cleared
+ ;; for further commands without giving "proof process
+ ;; busy" error.
(isa-update-thy-only buffer-file-name t t)
;; Leave the messages from the update around.
(setq proof-shell-erase-response-flag nil))))