# HG changeset patch
# User wenzelm
# Date 1216068948 -7200
# Node ID 6d81c734f7af69688b05f0a6e35679fedd344a22
# Parent  5e499b223a1e4b7fca8c2580481d0f540cd78f65
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;

diff -r 5e499b223a1e -r 6d81c734f7af 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);