render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
authorwenzelm
Thu, 05 Mar 2009 23:12:59 +0100
changeset 30292 a3bb22493f11
parent 30291 a1c3abf57068
child 30294 d6bffd97d8d5
render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
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")