diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-08-30 14:49:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-08-30 14:49:36 +0000 |
| commit | 0b8b1d98d4e447715c9a190e1e826396f190487d (patch) | |
| tree | 241b66286bf14572b8a6c148408b76ac34ec5ede | |
| parent | 2cd89d605f0c6d91d9426fd6467b2430dd6bc497 (diff) | |
Fix interrupt hook for PolyML 4 in recent Isabelle
| -rw-r--r-- | isa/isabelle-system.el | 6 |
1 files 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)))) |