added isabelle-verbatim;

fixed proof-shell-pre-interrupt-hook: use isabelle-verbatim;

1 files 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