more explicit message markup and rendering;

--- a/src/Pure/PIDE/command.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -60,10 +60,13 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Isabelle_Markup.Serial(i) =>
-              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              val st0 = copy(results = results + (i -> result))
+              val props = Position.purge(atts)
+              val result = XML.Elem(Markup(name, props), body)
+              val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+
+              val st0 = copy(results = results + (i -> result_message))
               val st1 =
-                if (Protocol.is_tracing(message)) st0
+                if (Protocol.is_tracing(result)) st0
                 else
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, result)))

--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -231,6 +231,16 @@
   val STDERR = "stderr"
   val EXIT = "exit"
 
+  val WRITELN_MESSAGE = "writeln_message"
+  val TRACING_MESSAGE = "tracing_message"
+  val WARNING_MESSAGE = "warning_message"
+  val ERROR_MESSAGE = "error_message"
+
+  val message: String => String =
+    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
+        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+      .withDefault((name: String) => name + "_message")
+
   val Return_Code = new Properties.Int("return_code")
 
   val LEGACY = "legacy"

--- a/src/Pure/PIDE/protocol.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -135,18 +135,21 @@
  def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
 
@@ -154,6 +157,8 @@
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
         List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
+        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
       case _ => false
     }
 

--- a/src/Tools/jEdit/etc/isabelle-jedit.css	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Tue Sep 18 17:20:40 2012 +0200
@@ -2,10 +2,10 @@
 
 .message { margin-top: 0.3ex; background-color: #F0F0F0; }
 
-.writeln { }
-.tracing { background-color: #F0F8FF; }
-.warning { background-color: #EEE8AA; }
-.error { background-color: #FFC1C1; }
+.writeln_message { }
+.tracing_message { background-color: #F0F8FF; }
+.warning_message { background-color: #EEE8AA; }
+.error_message { background-color: #FFC1C1; }
 
 .report { display: none; }
 

--- a/src/Tools/jEdit/etc/options	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 18 17:20:40 2012 +0200
@@ -31,6 +31,10 @@
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
+option writeln_message_color : string = "F0F0F0FF"
+option tracing_message_color : string = "F0F8FFFF"
+option warning_message_color : string = "EEE8AAFF"
+option error_message_color : string = "FFC1C1FF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -109,6 +109,10 @@
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
   val error1_color = color_value("error1_color")
+  val writeln_message_color = color_value("writeln_message_color")
+  val tracing_message_color = color_value("tracing_message_color")
+  val warning_message_color = color_value("warning_message_color")
+  val error_message_color = color_value("error_message_color")
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
   val quoted_color = color_value("quoted_color")
@@ -359,11 +363,21 @@
         Text.Info(r, result) <-
           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
             range, (Some(Protocol.Status.init), None),
-            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
+            Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
+              Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
+              Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
                 (Some(Protocol.command_status(status, markup)), color)
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _), _))) =>
+                (None, Some(writeln_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _))) =>
+                (None, Some(tracing_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _))) =>
+                (None, Some(warning_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _))) =>
+                (None, Some(error_message_color))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>

--- a/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -69,11 +69,8 @@
 
     val new_output =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2).filter(
-        { // FIXME not scalable
-          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
-          case _ => true
-        }).toList
+        new_state.results.iterator.map(_._2)
+          .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
       else current_output
 
     if (new_output != current_output)

--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 18 15:55:29 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 18 17:20:40 2012 +0200
@@ -100,11 +100,8 @@
 
     val new_body =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2).filter(
-        { // FIXME not scalable
-          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
-          case _ => true
-        }).toList
+        new_state.results.iterator.map(_._2)
+          .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
       else current_body
 
     if (new_body != current_body) html_panel.render(new_body)