--- 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
+ }
+ }
+ }
}
--- 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]] =
--- 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))
}
--- 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()