diff options
| -rw-r--r-- | generic/proof-config.el | 8 | ||||
| -rw-r--r-- | isar/isabelle-system.el | 9 |
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 ========== |