src/Pure/PIDE/protocol.scala
changeset 56306 0fc032898b05
parent 56299 8201790fdeb9
child 56335 8953d4cc060a
     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