From 46bfbbe644b09c7e331bde88bc7d7792e2fd4d43 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Sun, 4 Jun 2000 12:39:50 +0000
Subject: added isabelle-verbatim; fixed proof-shell-pre-interrupt-hook: use
 isabelle-verbatim;

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

diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index c79eff71..fffdb3a2 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -182,13 +182,20 @@ Called with one argument: t to save database, nil otherwise."
       (isa-insert-ret "quit();"))
   (comint-send-eof))
 
+(defconst isabelle-verbatim-regexp "^\^VERBATIM: \\(\\(.\\|\n\\)*\\)$"
+  "Regexp matching internal marker for verbatim command output")
+
+(defun isabelle-verbatim (str)
+  "Mark internal command for verbatim output"
+  (concat "\^VERBATIM: " str))
+
 ;;; Set proof-shell-pre-interrupt-hook for PolyML.
 (if (and
      (not proof-shell-pre-interrupt-hook)
      (string-match "^polyml" (isa-getenv "ML_SYSTEM")))
     (add-hook
      'proof-shell-pre-interrupt-hook
-     (lambda () (proof-shell-insert "f" nil))))
+     (lambda () (proof-shell-insert (isabelle-verbatim "f") nil))))
 
 ;;; ==========  Utility functions ==========
 
@@ -257,7 +264,7 @@ until Proof General is restarted."
   :type 'boolean
   :setting "trace_simp:=%b;")
 
-; FIXME: maybe for Isabelle99-1 ?
+; FIXME: for Isabelle99-1
 ; (defpacustom global-timing  nil
 ;  "Whether to enable timing in Isabelle."
 ;  :type 'boolean
@@ -281,7 +288,5 @@ until Proof General is restarted."
 (defpgdefault help-menu-entries isabelle-docs-menu)
 
 
-
-
 (provide 'isabelle-system)
 ;; End of isabelle-system.el
-- 
cgit v1.2.3