--- 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]] =