--- 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
+ }
+ }
+ }
}