Arrange for activate-scripting to not block for interactive calls.

3 files changed, 25 insertions, 7 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index d12977e7..2efe64af 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -849,7 +849,15 @@ The current buffer will be the newly active scripting buffer.
 This hook may be useful for synchronizing with the proof
 assistant, for example, to switch to a new theory
 (in case that isn't already done by commands in the proof
-script)."
+script).
+
+When functions in this hook are called, the variable
+`activated-interactively' will be non-nil if 
+proof-activate-scripting was called interactively
+(rather than as a side-effect of some other action).
+If a hook function sends commands to the proof process,
+it should wait for them to complete (so the queue is cleared
+for scripting commands), unless activated-interactively is set."
   :type '(repeat function)
   :group 'proof-script)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4481205e..0aa633b2 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -820,8 +820,13 @@ correct theory, or whatever."
 		(save-some-buffers)
  	      (set-buffer-modified-p modified))))
 
-      ;; Run hooks
-      (run-hooks 'proof-activate-scripting-hook)))))
+      ;; Run hooks with a variable which suggests whether or not 
+      ;; to block.   NB: The hook function may send commands to the
+      ;; process which will re-enter this function, but should exit 
+      ;; immediately because scripting has been turned on now.
+      (let
+	  ((activated-interactively	(interactive-p)))
+	(run-hooks 'proof-activate-scripting-hook))))))
 
 (defun proof-toggle-active-scripting (&optional arg)
   "Toggle active scripting mode in the current buffer.
@@ -834,9 +839,10 @@ With ARG, turn on scripting iff ARG is positive."
 	  (not (eq proof-script-buffer (current-buffer)))
 	(> (prefix-numeric-value arg) 0))
       (progn
-	(if proof-script-buffer (proof-deactivate-scripting))
-	(proof-activate-scripting))
-    (proof-deactivate-scripting)))
+	(if proof-script-buffer 
+	    (call-interactively (proof-deactivate-scripting)))
+	(call-interactively (proof-activate-scripting)))
+    (call-interactively (proof-deactivate-scripting))))
 
 ;; This function isn't such a wise idea: the buffer will often be fully
 ;; locked when writing a script, but we don't want to keep toggling
diff --git a/isa/isa.el b/isa/isa.el
index 72ea520f..04bb3baf 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -267,7 +267,11 @@ This is a hook function for proof-activate-scripting-hook."
 	;; 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)
+	(isa-update-thy-only buffer-file-name t 
+			     ;; whether to block or not
+			     (if (and (boundp 'activated-interactively)
+				      activated-interactively)
+				 nil t))
 	;; Leave the messages from the update around.
 	(setq proof-shell-erase-response-flag nil))))