# HG changeset patch
# User wenzelm
# Date 1236291179 -3600
# Node ID a3bb22493f11200bec0f5215fbb770efa873aab1
# Parent  a1c3abf57068e8243b66896a8fad26ac81c9191b
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;

diff -r a1c3abf57068 -r a3bb22493f11 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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")