# HG changeset patch
# User wenzelm
# Date 1395946050 -3600
# Node ID 0fc032898b056e80c929d8faf90032e1524c08b7
# Parent  06dcec23fb8dfc41283ebb040fc42fa354034e24
back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);

diff -r 06dcec23fb8d -r 0fc032898b05 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Mar 27 18:42:53 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 27 19:47:30 2014 +0100
@@ -74,8 +74,11 @@
       case _ => status
     }
 
-  def command_status(markups: List[Markup]): Status =
-    (Status.init /: markups)(command_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(_, _))
 
   val command_status_elements =
     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
@@ -119,13 +122,13 @@
     var failed = 0
     for {
       command <- node.commands
-      st <- state.command_states(version, command)
-      status = command_status(st.status)
+      states = state.command_states(version, command)
+      status = command_status(Status.init, states)
     } {
       if (status.is_running) running += 1
       else if (status.is_finished) {
-        if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
-        else finished += 1
+        val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
+        if (warning) warned += 1 else finished += 1
       }
       else if (status.is_failed) failed += 1
       else unprocessed += 1