proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which breaks Poly/MK 5;

2 files changed, 3 insertions, 14 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 0ca0155a..d8261e79 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2334,11 +2334,9 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'."
 
 (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."
+  "Run immediately after `comint-interrupt-subjob' is called.  This
+hook is added to allow customization for systems that query the user
+before returning to the top level."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 7e105bda..25abf308 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -250,15 +250,6 @@ Called with one argument: t to save database, nil otherwise."
   "Mark internal command for verbatim output"
   (concat "\^VERBATIM: " str))
 
-;;; Set proof-shell-pre-interrupt-hook for PolyML 3.
-(if (and
-     (not proof-shell-pre-interrupt-hook)
-     ;; (Older versions of Isabelle reported PolyML for PolyML 3).
-     (proof-string-match-safe "\\`polyml" (isa-getenv "ML_SYSTEM"))
-     (not (proof-string-match-safe "\\`polyml-4" (isa-getenv "ML_SYSTEM"))))
-    (add-hook
-     'proof-shell-pre-interrupt-hook
-     (lambda () (proof-shell-insert (isabelle-verbatim "f") nil))))
 
 ;;; ==========  Utility functions ==========