# HG changeset patch
# User wenzelm
# Date 1488747973 -3600
# Node ID 12c6774a8f65e71083669f4f81d028912d423ea5
# Parent  db6cc23fcf3319147ec4ee37d437a015f1a0b735
more generic rendering;

diff -r db6cc23fcf33 -r 12c6774a8f65 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Mar 05 19:27:39 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Mar 05 22:06:13 2017 +0100
@@ -32,6 +32,14 @@
     val quoted = Value("quoted")
     val antiquoted = Value("antiquoted")
     val foreground = values -- background
+
+    // 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
   }
 
 
@@ -61,6 +69,13 @@
     Markup.ERROR -> error_pri,
     Markup.ERROR_MESSAGE -> error_pri)
 
+  val message_underline_color = Map(
+    writeln_pri -> Color.writeln,
+    information_pri -> Color.information,
+    warning_pri -> Color.warning,
+    legacy_pri -> Color.legacy,
+    error_pri -> Color.error)
+
 
   /* markup elements */
 
@@ -344,4 +359,21 @@
     }
     else Nil
   }
+
+
+  /* message underline color */
+
+  def message_underline_color(
+    elements: Markup.Elements, range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
+  {
+    val results =
+      snapshot.cumulate[Int](range, 0, elements, _ =>
+        {
+          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
+        })
+    for {
+      Text.Info(r, pri) <- results
+      color <- Rendering.message_underline_color.get(pri)
+    } yield Text.Info(r, color)
+  }
 }
diff -r db6cc23fcf33 -r 12c6774a8f65 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 05 19:27:39 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 05 22:06:13 2017 +0100
@@ -178,10 +178,7 @@
   val running_color = color("running_color")
   val bullet_color = color("bullet_color")
   val tooltip_color = color("tooltip_color")
-  val writeln_color = color("writeln_color")
-  val information_color = color("information_color")
   val warning_color = color("warning_color")
-  val legacy_color = color("legacy_color")
   val error_color = color("error_color")
   val writeln_message_color = color("writeln_message_color")
   val information_message_color = color("information_message_color")
@@ -477,25 +474,8 @@
 
   /* squiggly underline */
 
-  private lazy val squiggly_colors = Map(
-    Rendering.writeln_pri -> writeln_color,
-    Rendering.information_pri -> information_color,
-    Rendering.warning_pri -> warning_color,
-    Rendering.legacy_pri -> legacy_color,
-    Rendering.error_pri -> error_color)
-
-  def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
-  {
-    val results =
-      snapshot.cumulate[Int](range, 0, JEdit_Rendering.squiggly_elements, _ =>
-        {
-          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
-        })
-    for {
-      Text.Info(r, pri) <- results
-      color <- squiggly_colors.get(pri)
-    } yield Text.Info(r, color)
-  }
+  def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
+    message_underline_color(JEdit_Rendering.squiggly_elements, range)
 
 
   /* message output */
diff -r db6cc23fcf33 -r 12c6774a8f65 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Mar 05 19:27:39 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Mar 05 22:06:13 2017 +0100
@@ -328,10 +328,10 @@
 
             // squiggly underline
             for {
-              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
+              Text.Info(range, c) <- rendering.squiggly_underline(line_range)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
-              gfx.setColor(color)
+              gfx.setColor(rendering.color(c))
               val x0 = (r.x / 2) * 2
               val y0 = r.y + fm.getAscent + 1
               for (x1 <- Range(x0, x0 + r.length, 2)) {