diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-02-09 19:41:59 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-02-09 19:41:59 +0000 |
| commit | 0309ccee40311b5684a79bcd5b3732a3aadc3952 (patch) | |
| tree | 2efc26dd0d72a2153895351971aa923ddc149f4f /generic | |
| parent | bfa4e7d1904022cd74a736e89a8a7367f95bc0d3 (diff) | |
Added proof-shell-pre-interrupt-hook
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 10 | ||||
| -rw-r--r-- | generic/proof-script.el | 3 |
2 files changed, 12 insertions, 1 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 3d85344f..36c97879 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1477,6 +1477,16 @@ determine whether the cause was an error or interrupt." :type '(repeat function) :group 'proof-shell) +(defcustom proof-shell-pre-interrupt-hook + nil + "Run immediately after `comint-interrupt-subjob' is called. +This hook is added to allow customization for Poly/ML and other +systems where the system queries the user before returning to +the top level. For Poly/ML it can be used to send the string \"f\", +for example." + :type '(repeat function) + :group 'proof-shell) + (defcustom proof-shell-process-output-system-specific nil "Set this variable to handle system specific output. Errors, start of proofs, abortions of proofs and completions of diff --git a/generic/proof-script.el b/generic/proof-script.el index 982de20e..ce97d623 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1790,7 +1790,8 @@ handling of interrupt signals." (with-current-buffer proof-shell-buffer ;; Just send an interrrupt. ;; Action on receiving one is triggered in proof-shell - (comint-interrupt-subjob))) + (comint-interrupt-subjob) + (run-hooks 'proof-shell-pre-interrupt-hook))) ;; |