xsymbols: use plain Symbol.output;
explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock);
Markup.no_output;

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jan 02 22:54:04 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jan 02 23:01:37 2009 +0100
@@ -23,75 +23,74 @@
 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 (fn (name, props) =>
-  if name = Markup.promptN then ("", "") else XML.output_markup (name, props));
-
 fun special ch = Symbol.SOH ^ ch;
 
 
-(* text output: print modes for xsymbol *)
+(* render markup *)
 
 local
 
-fun xsym_output "\\" = "\\\\"
-  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
-
-fun xsymbols_output s =
-  if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
-    let val syms = Symbol.explode s
-    in (implode (map xsym_output syms), Symbol.length syms) end
-  else Output.default_output s;
+fun render_trees ts = fold render_tree ts
+and render_tree (XML.Text s) = Buffer.add s
+  | render_tree (XML.Elem (name, props, ts)) =
+      let
+        val (bg1, en1) =
+          if name <> Markup.promptN andalso print_mode_active test_markupN
+          then XML.output_markup (name, props)
+          else Markup.no_output;
+        val (bg2, en2) =
+          if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output
+          else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+          else if name = Markup.sendbackN then (special "W", special "X")
+          else if name = Markup.hiliteN then (special "0", special "1")
+          else if name = Markup.tclassN then (special "B", special "A")
+          else if name = Markup.tfreeN then (special "C", special "A")
+          else if name = Markup.tvarN then (special "D", special "A")
+          else if name = Markup.freeN then (special "E", special "A")
+          else if name = Markup.boundN then (special "F", special "A")
+          else if name = Markup.varN then (special "G", special "A")
+          else if name = Markup.skolemN then (special "H", special "A")
+          else Markup.no_output;
+      in
+        Buffer.add bg1 #>
+        Buffer.add bg2 #>
+        render_trees ts #>
+        Buffer.add en2 #>
+        Buffer.add en1
+      end;
 
 in
 
-fun setup_xsymbols_output () =
-  Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
+fun render text =
+  Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
 
 end;
 
 
-(* common markup *)
+(* messages *)
+
+fun message bg en prfx text =
+  (case render text of
+    "" => ()
+  | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
 
-val _ = Markup.add_mode proof_generalN (fn (name, props) =>
-  let
-    val (bg1, en1) =
-      if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
-      else if name = Markup.sendbackN then (special "W", special "X")
-      else if name = Markup.hiliteN then (special "0", special "1")
-      else if name = Markup.tclassN then (special "B", special "A")
-      else if name = Markup.tfreeN then (special "C", special "A")
-      else if name = Markup.tvarN then (special "D", special "A")
-      else if name = Markup.freeN then (special "E", special "A")
-      else if name = Markup.boundN then (special "F", special "A")
-      else if name = Markup.varN then (special "G", special "A")
-      else if name = Markup.skolemN then (special "H", special "A")
-      else ("", "");
-    val (bg2, en2) =
-      if name <> Markup.promptN andalso print_mode_active test_markupN
-      then XML.output_markup (name, props)
-      else ("", "");
-  in (bg1 ^ bg2, en2 ^ en1) end);
+fun setup_messages () =
+ (Output.writeln_fn := message "" "" "";
+  Output.status_fn := (fn s => ! Output.priority_fn s);
+  Output.priority_fn := message (special "I") (special "J") "";
+  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.debug_fn := message (special "K") (special "L") "+++ ";
+  Output.warning_fn := message (special "K") (special "L") "### ";
+  Output.error_fn := message (special "M") (special "N") "*** ";
+  Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
+
+fun panic s =
+  (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
 
 
-(* messages and notification *)
-
-fun decorate bg en prfx =
-  Output.writeln_default o enclose bg en o prefix_lines prfx;
+(* notification *)
 
-fun setup_messages () =
- (Output.writeln_fn := Output.writeln_default;
-  Output.status_fn := (fn "" => () | s => ! Output.priority_fn s);
-  Output.priority_fn := (fn s => decorate (special "I") (special "J") "" s);
-  Output.tracing_fn := (fn s => decorate (special "I" ^ special "V") (special "J") "" s);
-  Output.debug_fn := (fn s => decorate (special "K") (special "L") "+++ " s);
-  Output.warning_fn := (fn s => decorate (special "K") (special "L") "### " s);
-  Output.error_fn := (fn s => decorate (special "M") (special "N") "*** " s);
-  Output.prompt_fn := (fn s => Output.std_output (s ^ special "S")));
-
-fun panic s =
-  (decorate (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-
-fun emacs_notify s = decorate (special "I") (special "J") "" s;
+val emacs_notify = message (special "I") (special "J") "";
 
 fun tell_clear_goals () =
   emacs_notify "Proof General, please clear the goals buffer.";
@@ -233,7 +232,9 @@
   | init true =
       (! initialized orelse
         (Output.no_warnings init_outer_syntax ();
-          setup_xsymbols_output ();
+          Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+          Output.add_mode proof_generalN Output.default_output Output.default_escape;
+          Markup.add_mode proof_generalN YXML.output_markup;
           setup_messages ();
           ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
           setup_thy_loader ();