# HG changeset patch
# User wenzelm
# Date 1495540051 -7200
# Node ID f97d163479b9ff26fe293ddebaf9ef5cec9ab359
# Parent  5bc7e080b18221586098e3ecfb079fa2e48f5feb
clarified modules;

diff -r 5bc7e080b182 -r f97d163479b9 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue May 23 11:47:35 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue May 23 13:47:31 2017 +0200
@@ -40,6 +40,10 @@
     val text_colors =
       values -- background_colors -- foreground_colors -- message_underline_colors --
       message_background_colors
+
+    // overview
+    val unprocessed, running = Value
+    val overview_colors = Set(unprocessed, running, error, warning)
   }
 
 
@@ -471,4 +475,29 @@
       if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
     }
   }
+
+
+  /* command status overview */
+
+  def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
+  {
+    if (snapshot.is_outdated) None
+    else {
+      val results =
+        snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
+          {
+            case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
+          }, status = true)
+      if (results.isEmpty) None
+      else {
+        val status = Protocol.Status.make(results.iterator.flatMap(_.info))
+
+        if (status.is_running) Some(Rendering.Color.running)
+        else if (status.is_failed) Some(Rendering.Color.error)
+        else if (status.is_warned) Some(Rendering.Color.warning)
+        else if (status.is_unprocessed) Some(Rendering.Color.unprocessed)
+        else None
+      }
+    }
+  }
 }
diff -r 5bc7e080b182 -r f97d163479b9 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue May 23 11:47:35 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue May 23 13:47:31 2017 +0200
@@ -174,12 +174,8 @@
   val main_color = jEdit.getColorProperty("view.fgColor")
 
   val outdated_color = color("outdated_color")
-  val unprocessed_color = color("unprocessed_color")
-  val running_color = color("running_color")
   val bullet_color = color("bullet_color")
   val tooltip_color = color("tooltip_color")
-  val warning_color = color("warning_color")
-  val error_color = color("error_color")
   val spell_checker_color = color("spell_checker_color")
   val entity_ref_color = color("entity_ref_color")
   val breakpoint_disabled_color = color("breakpoint_disabled_color")
@@ -251,31 +247,6 @@
         }).headOption.map(_.info)
 
 
-  /* command status overview */
-
-  def overview_color(range: Text.Range): Option[Color] =
-  {
-    if (snapshot.is_outdated) None
-    else {
-      val results =
-        snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
-          {
-            case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
-          }, status = true)
-      if (results.isEmpty) None
-      else {
-        val status = Protocol.Status.make(results.iterator.flatMap(_.info))
-
-        if (status.is_running) Some(running_color)
-        else if (status.is_failed) Some(error_color)
-        else if (status.is_warned) Some(warning_color)
-        else if (status.is_unprocessed) Some(unprocessed_color)
-        else None
-      }
-    }
-  }
-
-
   /* caret focus */
 
   def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
diff -r 5bc7e080b182 -r f97d163479b9 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 23 11:47:35 2017 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 23 13:47:31 2017 +0200
@@ -219,7 +219,8 @@
       text_area.getPainter.repaint()
     }
     text_field.setForeground(
-      if (ok) search_field_foreground else current_rendering.error_color)
+      if (ok) search_field_foreground
+      else current_rendering.color(Rendering.Color.error))
   }
 
 
diff -r 5bc7e080b182 -r f97d163479b9 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue May 23 11:47:35 2017 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue May 23 13:47:31 2017 +0200
@@ -69,8 +69,10 @@
 
   /* synchronous painting */
 
+  type Color_Info = (Rendering.Color.Value, Int, Int)
+
+  private var current_colors: List[Color_Info] = Nil
   private var current_overview = Overview()
-  private var current_colors: List[(Color, Int, Int)] = Nil
 
   private val delay_repaint =
     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
@@ -96,7 +98,7 @@
           gfx.setColor(getBackground)
           gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
           for ((color, h, h1) <- current_colors) {
-            gfx.setColor(color)
+            gfx.setColor(rendering.color(color))
             gfx.fillRect(0, h, getWidth, h1 - h)
           }
         }
@@ -138,8 +140,8 @@
                 val L = overview.L
                 val H = overview.H
 
-                @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
-                  : List[(Color, Int, Int)] =
+                @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[Color_Info])
+                  : List[Color_Info] =
                 {
                   Exn.Interrupt.expose()