# HG changeset patch
# User wenzelm
# Date 1488796686 -3600
# Node ID 759c64c39a6f1a2dd28eeaad05cf4cbe9e9b6e14
# Parent  4d088fe6185ec2c16442a5568951da50c0fbde4e
more generic colors;

diff -r 4d088fe6185e -r 759c64c39a6f src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Mar 06 11:38:06 2017 +0100
@@ -33,13 +33,23 @@
     val antiquoted = Value("antiquoted")
     val foreground = values -- background
 
-    // underline
+    // message underline
     val writeln = Value("writeln")
     val information = Value("information")
     val warning = Value("warning")
     val legacy = Value("legacy")
     val error = Value("error")
-    val underline = values -- background -- foreground
+    val message_underline = values -- background -- foreground
+
+    // message background
+
+    val writeln_message = Value("writeln_message")
+    val information_message = Value("information_message")
+    val tracing_message = Value("tracing_message")
+    val warning_message = Value("warning_message")
+    val legacy_message = Value("legacy_message")
+    val error_message = Value("error_message")
+    val message_background = values -- background -- foreground -- message_underline
   }
 
 
@@ -76,6 +86,14 @@
     legacy_pri -> Color.legacy,
     error_pri -> Color.error)
 
+  val message_background_color = Map(
+    writeln_pri -> Color.writeln_message,
+    information_pri -> Color.information_message,
+    tracing_pri -> Color.tracing_message,
+    warning_pri -> Color.warning_message,
+    legacy_pri -> Color.legacy_message,
+    error_pri -> Color.error_message)
+
 
   /* markup elements */
 
diff -r 4d088fe6185e -r 759c64c39a6f src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:38:06 2017 +0100
@@ -180,9 +180,7 @@
   val tooltip_color = color("tooltip_color")
   val warning_color = color("warning_color")
   val error_color = color("error_color")
-  val writeln_message_color = color("writeln_message_color")
   val information_message_color = color("information_message_color")
-  val tracing_message_color = color("tracing_message_color")
   val warning_message_color = color("warning_message_color")
   val legacy_message_color = color("legacy_message_color")
   val error_message_color = color("error_message_color")
@@ -480,15 +478,7 @@
 
   /* message output */
 
-  private lazy 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.legacy_pri -> legacy_message_color,
-    Rendering.error_pri -> error_message_color)
-
-  def line_background(range: Text.Range): Option[(Color, Boolean)] =
+  def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
   {
     val results =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
@@ -497,7 +487,7 @@
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
-    message_colors.get(pri).map(message_color =>
+    Rendering.message_background_color.get(pri).map(message_color =>
       {
         val is_separator =
           snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
diff -r 4d088fe6185e -r 759c64c39a6f src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 06 11:38:06 2017 +0100
@@ -300,9 +300,9 @@
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
             // line background color
-            for { (color, separator) <- rendering.line_background(line_range) }
+            for { (c, separator) <- rendering.line_background(line_range) }
             {
-              gfx.setColor(color)
+              gfx.setColor(rendering.color(c))
               val sep = if (separator) 2 min (line_height / 2) else 0
               gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
             }