back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);
1.1 --- a/src/Pure/PIDE/protocol.scala Thu Mar 27 18:42:53 2014 +0100
1.2 +++ b/src/Pure/PIDE/protocol.scala Thu Mar 27 19:47:30 2014 +0100
1.3 @@ -74,8 +74,11 @@
1.4 case _ => status
1.5 }
1.6
1.7 - def command_status(markups: List[Markup]): Status =
1.8 - (Status.init /: markups)(command_status(_, _))
1.9 + def command_status(status: Status, state: Command.State): Status =
1.10 + (status /: state.status)(command_status(_, _))
1.11 +
1.12 + def command_status(status: Status, states: List[Command.State]): Status =
1.13 + (status /: states)(command_status(_, _))
1.14
1.15 val command_status_elements =
1.16 Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
1.17 @@ -119,13 +122,13 @@
1.18 var failed = 0
1.19 for {
1.20 command <- node.commands
1.21 - st <- state.command_states(version, command)
1.22 - status = command_status(st.status)
1.23 + states = state.command_states(version, command)
1.24 + status = command_status(Status.init, states)
1.25 } {
1.26 if (status.is_running) running += 1
1.27 else if (status.is_finished) {
1.28 - if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
1.29 - else finished += 1
1.30 + val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
1.31 + if (warning) warned += 1 else finished += 1
1.32 }
1.33 else if (status.is_failed) failed += 1
1.34 else unprocessed += 1