# HG changeset patch
# User wenzelm
# Date 1349425429 -7200
# Node ID f7b636d364968942022461ca401187e77f3e0c35
# Parent  c89fffb11769356932b41c63c65c2fcc04d0be81
proper message markup for output;

diff -r c89fffb11769 -r f7b636d36496 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Oct 04 20:36:10 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Oct 05 10:23:49 2012 +0200
@@ -266,12 +266,12 @@
         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
           Isabelle_Markup.BAD)),
         {
-          case (msgs, Text.Info(_, msg @
-              XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
-          if markup == Isabelle_Markup.WRITELN ||
-              markup == Isabelle_Markup.WARNING ||
-              markup == Isabelle_Markup.ERROR =>
-            msgs + (serial -> msg)
+          case (msgs, Text.Info(_,
+            XML.Elem(Markup(name, props @ Isabelle_Markup.Serial(serial)), body)))
+          if name == Isabelle_Markup.WRITELN ||
+              name == Isabelle_Markup.WARNING ||
+              name == Isabelle_Markup.ERROR =>
+            msgs + (serial -> XML.Elem(Markup(Isabelle_Markup.message(name), props), body))
           case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
           if !body.isEmpty => msgs + (Document.new_id() -> msg)
         }).toList.flatMap(_.info)