print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
authorwenzelm
Mon, 14 Jul 2008 22:55:48 +0200
changeset 27592 6d81c734f7af
parent 27591 5e499b223a1e
child 27593 602dd4b219c0
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 22:26:53 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 22:55:48 2008 +0200
@@ -25,7 +25,8 @@
 val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
 val test_markupN = "test_markup";          (*XML markup for everything*)
 
-val _ = Markup.add_mode test_markupN XML.output_markup;
+val _ = Markup.add_mode test_markupN (fn (name, props) =>
+  if name = Markup.promptN then ("", "") else XML.output_markup (name, props));
 
 fun special oct =
   if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
@@ -70,7 +71,7 @@
       else if name = Markup.skolemN then (special "357", special "350")
       else ("", "");
     val (bg2, en2) =
-      if print_mode_active test_markupN
+      if name <> Markup.promptN andalso print_mode_active test_markupN
       then XML.output_markup (name, props)
       else ("", "");
   in (bg1 ^ bg2, en2 ^ en1) end);