From 0309ccee40311b5684a79bcd5b3732a3aadc3952 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 9 Feb 2000 19:41:59 +0000
Subject: Added proof-shell-pre-interrupt-hook

---
 generic/proof-config.el | 10 ++++++++++
 generic/proof-script.el |  3 ++-
 2 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'generic')

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)))
   
 
 ;;
-- 
cgit v1.2.3