--- a/src/Pure/PIDE/protocol.scala Mon Jan 09 23:09:03 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Jan 09 23:11:28 2012 +0100
@@ -43,24 +43,32 @@
/* toplevel transactions */
- sealed abstract class Status
- case object Unprocessed extends Status
- case class Forked(forks: Int) extends Status
- case object Finished extends Status
- case object Failed extends Status
-
- def command_status(markup: List[Markup]): Status =
+ sealed case class Status(
+ private val finished: Boolean = false,
+ private val failed: Boolean = false,
+ forks: Int = 0)
{
- val forks = (0 /: markup) {
- case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
- case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
- case (i, _) => i
+ def is_unprocessed: Boolean = !finished && !failed && forks == 0
+ def is_running: Boolean = forks != 0
+ def is_finished: Boolean = finished && forks == 0
+ def is_failed: Boolean = failed && forks == 0
+ }
+
+ val command_status_markup: Set[String] =
+ Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
+ Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
+
+ def command_status(status: Status, markup: Markup): Status =
+ markup match {
+ case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
+ case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
+ case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
+ case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
+ case _ => status
}
- if (forks != 0) Forked(forks)
- else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
- else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
- else Unprocessed
- }
+
+ def command_status(markups: List[Markup]): Status =
+ (Status() /: markups)(command_status(_, _))
sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
{
@@ -75,11 +83,12 @@
var finished = 0
var failed = 0
node.commands.foreach(command =>
- command_status(state.command_state(version, command).status) match {
- case Unprocessed => unprocessed += 1
- case Forked(_) => running += 1
- case Finished => finished += 1
- case Failed => failed += 1
+ {
+ val status = command_status(state.command_state(version, command).status)
+ if (status.is_running) running += 1
+ else if (status.is_finished) finished += 1
+ else if (status.is_failed) failed += 1
+ else unprocessed += 1
})
Node_Status(unprocessed, running, finished, failed)
}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Jan 09 23:09:03 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Jan 09 23:11:28 2012 +0100
@@ -26,10 +26,10 @@
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
val outdated_color = new Color(238, 227, 227)
+ val unprocessed_color = new Color(255, 160, 160)
+ val unprocessed1_color = new Color(255, 160, 160, 50)
val running_color = new Color(97, 0, 97)
val running1_color = new Color(97, 0, 97, 100)
- val unprocessed_color = new Color(255, 160, 160)
- val unprocessed1_color = new Color(255, 160, 160, 50)
val light_color = new Color(240, 240, 240)
val regular_color = new Color(192, 192, 192)
@@ -54,34 +54,25 @@
val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
- /* command status */
-
- def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
- {
- val state = snapshot.command_state(command)
- if (snapshot.is_outdated) Some(outdated_color)
- else
- Protocol.command_status(state.status) match {
- case Protocol.Forked(i) if i > 0 => Some(running1_color)
- case Protocol.Unprocessed => Some(unprocessed1_color)
- case _ => None
- }
- }
+ /* command overview */
def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
{
val state = snapshot.command_state(command)
if (snapshot.is_outdated) None
- else
- Protocol.command_status(state.status) match {
- case Protocol.Forked(i) => if (i > 0) Some(running_color) else None
- case Protocol.Unprocessed => Some(unprocessed_color)
- case Protocol.Failed => Some(error_color)
- case Protocol.Finished =>
- if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
- else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
- else None
+ else {
+ val status = Protocol.command_status(state.status)
+
+ if (status.is_unprocessed) Some(unprocessed_color)
+ else if (status.is_running) Some(running_color)
+ else if (status.is_finished) {
+ if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
+ else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
+ else None
}
+ else if (status.is_failed) Some(error_color)
+ else None
+ }
}
@@ -121,12 +112,18 @@
Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
val background1 =
- Markup_Tree.Select[Color](
+ Markup_Tree.Cumulate[(Option[Protocol.Status], Option[Color])](
+ (Some(Protocol.Status()), None),
{
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _)) => bad_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _)) => hilite_color
+ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ if (Protocol.command_status_markup(markup.name)) =>
+ (Some(Protocol.command_status(status, markup)), color)
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
+ (None, Some(bad_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
+ (None, Some(hilite_color))
},
- Some(Set(Isabelle_Markup.BAD, Isabelle_Markup.HILITE)))
+ Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE))
val background2 =
Markup_Tree.Select[Color](
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Jan 09 23:09:03 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Jan 09 23:11:28 2012 +0100
@@ -89,29 +89,27 @@
if (physical_lines(i) != -1) {
val line_range = doc_view.proper_line_range(start(i), end(i))
- // background color: status
+ // background color (1)
for {
- (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range))
- if !command.is_ignored
- range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
- r <- Isabelle.gfx_range(text_area, range)
- color <- Isabelle_Rendering.status_color(snapshot, command)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // background color (1): markup
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Rendering.background1).iterator
+ Text.Info(range, result) <-
+ snapshot.cumulate_markup(line_range)(Isabelle_Rendering.background1).iterator
+ // FIXME more abstract Isabelle_Rendering.markup etc.
+ val opt_color =
+ result match {
+ case (Some(status), _) =>
+ if (status.is_running) Some(Isabelle_Rendering.running1_color)
+ else if (status.is_unprocessed) Some(Isabelle_Rendering.unprocessed1_color)
+ else None
+ case (_, color) => color
+ }
+ color <- opt_color
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
- // background color (2): markup
+ // background color (2)
for {
Text.Info(range, Some(color)) <-
snapshot.select_markup(line_range)(Isabelle_Rendering.background2).iterator