Move setting of proof-shell-pre-interrupt-hook to isabelle-system.el

3 files changed, 7 insertions, 10 deletions

diff --git a/isa/interface-setup.el b/isa/interface-setup.el
index 0a3f6b80..7e5ed4e4 100644
--- a/isa/interface-setup.el
+++ b/isa/interface-setup.el
@@ -6,11 +6,6 @@
  'isabelle-prog-name
  (concat (getenv "ISABELLE") " " (getenv "PROOFGENERAL_LOGIC")))
 
-(if (string-match "^polyml" (getenv "ML_SYSTEM"))
-    (customize-set-variable
-     'proof-shell-pre-interrupt-hook
-     (lambda () (proof-shell-insert "f" nil))))
-
 (let ((xsym (getenv "PROOFGENERAL_XSYMBOL")))
   (cond
    ((equal xsym "true")
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index bc2209ad..57cd4db6 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -182,6 +182,13 @@ Called with one argument: t to save database, nil otherwise."
       (isa-insert-ret "quit();"))
   (comint-send-eof))
 
+;;; Set proof-shell-pre-interrupt-hook for PolyML.
+(if (and
+     (not proof-shell-pre-interrupt-hook)
+     (string-match "^polyml" (isa-getenv "ML_SYSTEM")))
+    (add-hook
+     'proof-shell-pre-interrupt-hook
+     (lambda () (proof-shell-insert "f" nil))))
 
 ;;; ==========  Utility functions ==========
 
diff --git a/isar/interface-setup.el b/isar/interface-setup.el
index 76f4f09e..9fdaba2b 100644
--- a/isar/interface-setup.el
+++ b/isar/interface-setup.el
@@ -6,11 +6,6 @@
  'isabelle-isar-prog-name
  (concat (getenv "ISABELLE") " " (getenv "PROOFGENERAL_LOGIC")))
 
-(if (string-match "^polyml" (getenv "ML_SYSTEM"))
-    (customize-set-variable
-     'proof-shell-pre-interrupt-hook
-     (lambda () (proof-shell-insert (isar-verbatim "f") nil))))
-
 (let ((xsym (getenv "PROOFGENERAL_XSYMBOL")))
   (cond
    ((equal xsym "true")