diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2006-12-07 19:51:33 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2006-12-07 19:51:33 +0000 |
| commit | a4b24e4e30d10a79f3d8fc90d1acd69b80b4c2ab (patch) | |
| tree | 145672aed12d42374153122d2dafff4b39ef652b /isar/isabelle-system.el | |
| parent | 07559fb1fa3cad5e3fdd2fd5b14313e7ad455c9b (diff) | |
proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which breaks Poly/MK 5;
Diffstat (limited to 'isar/isabelle-system.el')
| -rw-r--r-- | isar/isabelle-system.el | 9 |
1 files changed, 0 insertions, 9 deletions
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 ========== |