src/Pure/PIDE/rendering.scala
changeset 65911 f97d163479b9
parent 65637 e9b87bf6578b
child 65913 f330f538dae6
--- 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
+      }
+    }
+  }
 }