src/Pure/PIDE/protocol.scala
changeset 57843 d8966c09025c
parent 56801 8dd9df88f647
child 57911 dcb758188aa6
equal deleted inserted replaced
57842:8e4ae2db1849 57843:d8966c09025c
   143     for (command <- node.commands.iterator) {
   143     for (command <- node.commands.iterator) {
   144       val states = state.command_states(version, command)
   144       val states = state.command_states(version, command)
   145       val status = Status.merge(states.iterator.map(_.protocol_status))
   145       val status = Status.merge(states.iterator.map(_.protocol_status))
   146 
   146 
   147       if (status.is_running) running += 1
   147       if (status.is_running) running += 1
       
   148       else if (status.is_failed) failed += 1
   148       else if (status.is_warned) warned += 1
   149       else if (status.is_warned) warned += 1
   149       else if (status.is_failed) failed += 1
       
   150       else if (status.is_finished) finished += 1
   150       else if (status.is_finished) finished += 1
   151       else unprocessed += 1
   151       else unprocessed += 1
   152     }
   152     }
   153     Node_Status(unprocessed, running, warned, failed, finished)
   153     Node_Status(unprocessed, running, warned, failed, finished)
   154   }
   154   }