diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-09 11:43:51 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-09 11:43:51 +0000 |
| commit | 094f4a516bce4f4409f42866d133113f009caf51 (patch) | |
| tree | def483a49f081faa20f333b05a83fde10e879f28 /generic/proof-script.el | |
| parent | ac6a40fd23e93c24f5af3762231afdbe61f611ef (diff) | |
Arrange for activate-scripting to not block for interactive calls.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 16 |
1 files changed, 11 insertions, 5 deletions
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 |