1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 26 21:01:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 27 10:43:43 2014 +0100
     1.3 @@ -117,18 +117,19 @@
     1.4      var finished = 0
     1.5      var warned = 0
     1.6      var failed = 0
     1.7 -    node.commands.foreach(command =>
     1.8 -      {
     1.9 -        val st = state.command_state(version, command)
    1.10 -        val status = command_status(st.status)
    1.11 -        if (status.is_running) running += 1
    1.12 -        else if (status.is_finished) {
    1.13 -          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
    1.14 -          else finished += 1
    1.15 -        }
    1.16 -        else if (status.is_failed) failed += 1
    1.17 -        else unprocessed += 1
    1.18 -      })
    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 +    } {
    1.24 +      if (status.is_running) running += 1
    1.25 +      else if (status.is_finished) {
    1.26 +        if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
    1.27 +        else finished += 1
    1.28 +      }
    1.29 +      else if (status.is_failed) failed += 1
    1.30 +      else unprocessed += 1
    1.31 +    }
    1.32      Node_Status(unprocessed, running, finished, warned, failed)
    1.33    }
    1.34  
    1.35 @@ -149,7 +150,7 @@
    1.36      var commands = Map.empty[Command, Double]
    1.37      for {
    1.38        command <- node.commands.iterator
    1.39 -      st = state.command_state(version, command)
    1.40 +      st <- state.command_states(version, command)
    1.41        command_timing =
    1.42          (0.0 /: st.status)({
    1.43            case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds