From 0b8b1d98d4e447715c9a190e1e826396f190487d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 30 Aug 2001 14:49:36 +0000
Subject: Fix interrupt hook for PolyML 4 in recent Isabelle

---
 isa/isabelle-system.el | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 9849f1bf..7cadc19a 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -204,10 +204,12 @@ 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.
+;;; Set proof-shell-pre-interrupt-hook for PolyML 3.
 (if (and
      (not proof-shell-pre-interrupt-hook)
-     (proof-string-match "\\`polyml" (isa-getenv "ML_SYSTEM")))
+     ;; (Older versions of Isabelle reported PolyML for PolyML 3).
+     (proof-string-match "\\`polyml" (isa-getenv "ML_SYSTEM"))
+     (not (proof-string-match "\\`polyml-4" (isa-getenv "ML_SYSTEM"))))
     (add-hook
      'proof-shell-pre-interrupt-hook
      (lambda () (proof-shell-insert (isabelle-verbatim "f") nil))))
-- 
cgit v1.2.3