From a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 7 Dec 2006 19:51:33 +0000
Subject: proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup,
 which breaks Poly/MK 5;

---
 isar/isabelle-system.el | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'isar')

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