# HG changeset patch # User wenzelm # Date 1326147088 -3600 # Node ID 4beb2f41ed9356bb2e4ec257f3e0654d635e2b55 # Parent 0e131ca93a492248bf45f8c7cd6a4407bea937fd command status color via regular markup; diff -r 0e131ca93a49 -r 4beb2f41ed93 src/Pure/PIDE/protocol.scala --- 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) } diff -r 0e131ca93a49 -r 4beb2f41ed93 src/Tools/jEdit/src/isabelle_rendering.scala --- 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]( diff -r 0e131ca93a49 -r 4beb2f41ed93 src/Tools/jEdit/src/text_area_painter.scala --- 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