render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 05 21:06:59 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 05 23:12:59 2009 +0100
@@ -39,7 +39,7 @@
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
+ if null ts 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")