--- a/src/Pure/PIDE/command.scala Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Pure/PIDE/command.scala Wed Apr 02 12:26:11 2014 +0200
@@ -109,13 +109,11 @@
results: Results = Results.empty,
markups: Markups = Markups.empty)
{
- /* markup */
+ lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
def markup(index: Markup_Index): Markup_Tree = markups(index)
- /* content */
-
def eq_content(other: State): Boolean =
command.source == other.command.source &&
status == other.status &&
--- a/src/Pure/PIDE/protocol.scala Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Apr 02 12:26:11 2014 +0200
@@ -41,6 +41,39 @@
/* command status */
+ object Status
+ {
+ def make(markup_iterator: Iterator[Markup]): Status =
+ {
+ var touched = false
+ var accepted = false
+ var failed = false
+ var forks = 0
+ var runs = 0
+ for (markup <- markup_iterator) {
+ markup.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 empty = make(Iterator.empty)
+
+ def merge(status_iterator: Iterator[Status]): Status =
+ if (status_iterator.hasNext) {
+ val status0 = status_iterator.next
+ (status0 /: status_iterator)(_ + _)
+ }
+ else empty
+ }
+
sealed case class Status(
private val touched: Boolean,
private val accepted: Boolean,
@@ -48,33 +81,16 @@
forks: Int,
runs: Int)
{
+ def + (that: Status): Status =
+ Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
+ forks + that.forks, runs + that.runs)
+
def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
def is_running: Boolean = runs != 0
def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
def is_failed: Boolean = failed
}
- 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) {
- markup.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,
Markup.FINISHED, Markup.FAILED)
@@ -117,7 +133,7 @@
var failed = 0
for (command <- node.commands.iterator) {
val states = state.command_states(version, command)
- val status = command_status(states.iterator.flatMap(st => st.status.iterator))
+ val status = Status.merge(states.iterator.map(_.protocol_status))
if (status.is_running) running += 1
else if (status.is_finished) {
--- a/src/Tools/jEdit/src/rendering.scala Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Apr 02 12:26:11 2014 +0200
@@ -304,7 +304,7 @@
if (results.isEmpty) None
else {
val status =
- Protocol.command_status(results.iterator.flatMap(info => info.info._1.iterator))
+ Protocol.Status.make(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)
@@ -628,7 +628,7 @@
color <-
(result match {
case (markups, opt_color) if !markups.isEmpty =>
- val status = Protocol.command_status(markups.iterator)
+ val status = Protocol.Status.make(markups.iterator)
if (status.is_unprocessed) Some(unprocessed1_color)
else if (status.is_running) Some(running1_color)
else opt_color