# HG changeset patch
# User wenzelm
# Date 1348171057 -7200
# Node ID e7ff10e1a15507d3e5e3775050aa340a37cebfa0
# Parent  ca7e2c21b10444b158ec8d6dab5c0ea643eca480
clarified message background;

diff -r ca7e2c21b104 -r e7ff10e1a155 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Sep 20 21:31:56 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Sep 20 21:57:37 2012 +0200
@@ -31,8 +31,7 @@
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
-option message_color : string = "F0F0F0FF"
-option writeln_message_color : string = "FFFFFF00"
+option writeln_message_color : string = "F0F0F0FF"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
diff -r ca7e2c21b104 -r e7ff10e1a155 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 21:31:56 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Sep 20 21:57:37 2012 +0200
@@ -29,9 +29,16 @@
   /* message priorities */
 
   private val writeln_pri = 1
-  private val warning_pri = 2
-  private val legacy_pri = 3
-  private val error_pri = 4
+  private val tracing_pri = 2
+  private val warning_pri = 3
+  private val legacy_pri = 4
+  private val error_pri = 5
+
+  private val message_pri = Map(
+    Isabelle_Markup.WRITELN -> writeln_pri, Isabelle_Markup.WRITELN_MESSAGE -> writeln_pri,
+    Isabelle_Markup.TRACING -> tracing_pri, Isabelle_Markup.TRACING_MESSAGE -> tracing_pri,
+    Isabelle_Markup.WARNING -> warning_pri, Isabelle_Markup.WARNING_MESSAGE -> warning_pri,
+    Isabelle_Markup.ERROR -> error_pri, Isabelle_Markup.ERROR_MESSAGE -> error_pri)
 
 
   /* icons */
@@ -109,7 +116,6 @@
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
   val error1_color = color_value("error1_color")
-  val message_color = color_value("message_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")
@@ -147,10 +153,8 @@
           Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
           {
             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
-              if (markup.name == Isabelle_Markup.WARNING)
-                (status, pri max Isabelle_Rendering.warning_pri)
-              else if (markup.name == Isabelle_Markup.ERROR)
-                (status, pri max Isabelle_Rendering.error_pri)
+              if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR)
+                (status, pri max Isabelle_Rendering.message_pri(markup.name))
               else (Protocol.command_status(status, markup), pri)
           })
       if (results.isEmpty) None
@@ -341,13 +345,10 @@
       snapshot.cumulate_markup[Int](range, 0,
         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
         {
-          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
-            name match {
-              case Isabelle_Markup.WRITELN => pri max Isabelle_Rendering.writeln_pri
-              case Isabelle_Markup.WARNING => pri max Isabelle_Rendering.warning_pri
-              case Isabelle_Markup.ERROR => pri max Isabelle_Rendering.error_pri
-              case _ => pri
-            }
+          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+          if name == Isabelle_Markup.WRITELN ||
+            name == Isabelle_Markup.WARNING ||
+            name == Isabelle_Markup.ERROR => pri max Isabelle_Rendering.message_pri(name)
         })
     for {
       Text.Info(r, pri) <- results
@@ -355,24 +356,36 @@
     } yield Text.Info(r, color)
   }
 
+
+  private val message_colors = Map(
+    Isabelle_Rendering.writeln_pri -> writeln_message_color,
+    Isabelle_Rendering.tracing_pri -> tracing_message_color,
+    Isabelle_Rendering.warning_pri -> warning_message_color,
+    Isabelle_Rendering.error_pri -> error_message_color)
+
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val messages =
-      Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.WARNING_MESSAGE,
-        Isabelle_Markup.ERROR_MESSAGE)
-    val is_message =
-      snapshot.cumulate_markup[Boolean](range, false, Some(messages),
+      Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
+        Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
+    val results =
+      snapshot.cumulate_markup[Int](range, 0, Some(messages),
         {
-          case (_, Text.Info(_, XML.Elem(Markup(name, _), body))) if messages(name) => true
-        }).exists(_.info)
-    val is_separator = is_message &&
-      snapshot.cumulate_markup[Boolean](range, false,
-        Some(Set(Isabelle_Markup.SEPARATOR)),
+          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+          if name == Isabelle_Markup.WRITELN_MESSAGE ||
+            name == Isabelle_Markup.TRACING_MESSAGE ||
+            name == Isabelle_Markup.WARNING_MESSAGE ||
+            name == Isabelle_Markup.ERROR_MESSAGE => pri max Isabelle_Rendering.message_pri(name)
+        })
+    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
+
+    val is_separator = pri > 0 &&
+      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Isabelle_Markup.SEPARATOR)),
         {
           case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
         }).exists(_.info)
 
-    if (is_message) Some((message_color, is_separator)) else None
+    message_colors.get(pri).map((_, is_separator))
   }
 
   def background1(range: Text.Range): Stream[Text.Info[Color]] =
@@ -390,14 +403,6 @@
               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, _), _))) =>