more rendering for information messages;

--- a/src/Pure/PIDE/protocol.scala	Sat Jul 13 17:05:22 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Jul 13 18:13:09 2013 +0200
@@ -205,15 +205,18 @@
       case _ => false
     }
 
-  def is_state(msg: XML.Tree): Boolean =
+  def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WRITELN, _),
-        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+        List(XML.Elem(markup, _))) => markup.name == name
       case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
-        List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+        List(XML.Elem(markup, _))) => markup.name == name
       case _ => false
     }
 
+  def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
+  def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true

--- a/src/Tools/jEdit/etc/options	Sat Jul 13 17:05:22 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Jul 13 18:13:09 2013 +0200
@@ -42,16 +42,17 @@
 option bullet_color : string = "000000FF"
 option tooltip_color : string = "FFFFE9FF"
 option writeln_color : string = "C0C0C0FF"
+option information_color : string = "C1DFEEFF"
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
 option writeln_message_color : string = "F0F0F0FF"
+option information_message_color : string = "C1DFEE32"
 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 information_color : string = "FFCC6632"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option highlight_color : string = "50505032"

--- a/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 17:05:22 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Jul 13 18:13:09 2013 +0200
@@ -124,16 +124,17 @@
   val bullet_color = color_value("bullet_color")
   val tooltip_color = color_value("tooltip_color")
   val writeln_color = color_value("writeln_color")
+  val information_color = color_value("information_color")
   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 information_message_color = color_value("information_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 information_color = color_value("information_color")
   val quoted_color = color_value("quoted_color")
   val antiquoted_color = color_value("antiquoted_color")
   val highlight_color = color_value("highlight_color")
@@ -416,6 +417,7 @@
 
   private val squiggly_colors = Map(
     Rendering.writeln_pri -> writeln_color,
+    Rendering.information_pri -> information_color,
     Rendering.warning_pri -> warning_color,
     Rendering.error_pri -> error_color)
 
@@ -426,10 +428,12 @@
     val results =
       snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
         {
-          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+          case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
           if name == Markup.WRITELN ||
             name == Markup.WARNING ||
-            name == Markup.ERROR => pri max Rendering.message_pri(name)
+            name == Markup.ERROR =>
+              if (Protocol.is_information(msg)) pri max Rendering.information_pri
+              else pri max Rendering.message_pri(name)
         })
     for {
       Text.Info(r, pri) <- results
@@ -438,20 +442,24 @@
   }
 
 
-  private val messages_include =
-    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
-
   private val message_colors = Map(
     Rendering.writeln_pri -> writeln_message_color,
+    Rendering.information_pri -> information_message_color,
     Rendering.tracing_pri -> tracing_message_color,
     Rendering.warning_pri -> warning_message_color,
     Rendering.error_pri -> error_message_color)
 
+  private val line_background_elements =
+    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
+      Markup.ERROR_MESSAGE, Markup.INFORMATION)
+
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
+      snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
         {
+          case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
+            pri max Rendering.information_pri
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Markup.WRITELN_MESSAGE ||
             name == Markup.TRACING_MESSAGE ||
@@ -478,8 +486,8 @@
 
   private val background1_include =
     Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
-      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
-      Markup.INFORMATION ++ active_include
+      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+      active_include
 
   def background1(range: Text.Range): Stream[Text.Info[Color]] =
   {
@@ -497,8 +505,6 @@
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                 (None, Some(intensify_color))
-              case (_, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
-                (None, Some(information_color))
               case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                 command_state.results.get(serial) match {
                   case Some(Protocol.Dialog_Result(res)) if res == result =>