--- a/src/Pure/PIDE/protocol.scala Tue Apr 01 16:16:25 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Apr 01 17:26:32 2014 +0200
@@ -41,17 +41,12 @@
/* command status */
- object Status
- {
- val init = Status()
- }
-
sealed case class Status(
- private val touched: Boolean = false,
- private val accepted: Boolean = false,
- private val failed: Boolean = false,
- forks: Int = 0,
- runs: Int = 0)
+ private val touched: Boolean,
+ private val accepted: Boolean,
+ private val failed: Boolean,
+ forks: Int,
+ runs: Int)
{
def + (that: Status): Status =
Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
@@ -63,22 +58,25 @@
def is_failed: Boolean = failed
}
- def command_status(status: Status, markup: Markup): Status =
- markup match {
- case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
- case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
- case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
- case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
- case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
- case Markup(Markup.FAILED, _) => status.copy(failed = true)
- case _ => status
- }
-
- def command_status(status: Status, state: Command.State): Status =
- (status /: state.status)(command_status(_, _))
-
- def command_status(status: Status, states: List[Command.State]): Status =
- (status /: states)(command_status(_, _))
+ def command_status(markups: Iterator[Markup]): Status =
+ {
+ var touched = false
+ var accepted = false
+ var failed = false
+ var forks = 0
+ var runs = 0
+ for { markup <- markups; name = markup.name }
+ name match {
+ case Markup.ACCEPTED => accepted = true
+ case Markup.FORKED => touched = true; forks += 1
+ case Markup.JOINED => forks -= 1
+ case Markup.RUNNING => touched = true; runs += 1
+ case Markup.FINISHED => runs -= 1
+ case Markup.FAILED => failed = true
+ case _ =>
+ }
+ Status(touched, accepted, failed, forks, runs)
+ }
val command_status_elements =
Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
@@ -123,7 +121,7 @@
for {
command <- node.commands
states = state.command_states(version, command)
- status = command_status(Status.init, states)
+ status = command_status(states.iterator.flatMap(st => st.status.iterator))
} {
if (status.is_running) running += 1
else if (status.is_finished) {
--- a/src/Tools/jEdit/src/rendering.scala Tue Apr 01 16:16:25 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Tue Apr 01 17:26:32 2014 +0200
@@ -292,20 +292,20 @@
if (snapshot.is_outdated) None
else {
val results =
- snapshot.cumulate[(Protocol.Status, Int)](
- range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
+ snapshot.cumulate[(List[Markup], Int)](
+ range, (Nil, 0), Protocol.status_elements, _ =>
{
case ((status, pri), Text.Info(_, elem)) =>
if (Protocol.command_status_elements(elem.name))
- Some((Protocol.command_status(status, elem.markup), pri))
+ Some((elem.markup :: status), pri)
else
Some((status, pri max Rendering.message_pri(elem.name)))
}, status = true)
if (results.isEmpty) None
else {
- val (status, pri) =
- ((Protocol.Status.init, 0) /: results) {
- case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
+ val status =
+ Protocol.command_status(results.iterator.flatMap(info => info.info._1.iterator))
+ val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _)
if (status.is_running) Some(running_color)
else if (pri == Rendering.warning_pri) Some(warning_color)
@@ -604,31 +604,32 @@
else
for {
Text.Info(r, result) <-
- snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status.init), None), Rendering.background_elements,
+ snapshot.cumulate[(List[Markup], Option[Color])](
+ range, (List(Markup.Empty), None), Rendering.background_elements,
command_results =>
{
- case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
- if (Protocol.command_status_elements(markup.name)) =>
- Some((Some(Protocol.command_status(status, markup)), color))
+ case (((status, color), Text.Info(_, XML.Elem(markup, _))))
+ if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
+ Some((markup :: status, color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
- Some((None, Some(bad_color)))
+ Some((Nil, Some(bad_color)))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
- Some((None, Some(intensify_color)))
+ Some((Nil, Some(intensify_color)))
case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
command_results.get(serial) match {
case Some(Protocol.Dialog_Result(res)) if res == result =>
- Some((None, Some(active_result_color)))
+ Some((Nil, Some(active_result_color)))
case _ =>
- Some((None, Some(active_color)))
+ Some((Nil, Some(active_color)))
}
case (_, Text.Info(_, elem)) =>
- if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
+ if (Rendering.active_elements(elem.name)) Some((Nil, Some(active_color)))
else None
})
color <-
(result match {
- case (Some(status), opt_color) =>
+ case (markups, opt_color) if !markups.isEmpty =>
+ val status = Protocol.command_status(markups.iterator)
if (status.is_unprocessed) Some(unprocessed1_color)
else if (status.is_running) Some(running1_color)
else opt_color