diff options
| -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))) ;; |