src/Pure/PIDE/protocol.scala
changeset 56352 abdc524db8b4
parent 56335 8953d4cc060a
child 56353 ecbdfe30bf7f
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 16:16:25 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 17:26:32 2014 +0200
     1.3 @@ -41,17 +41,12 @@
     1.4  
     1.5    /* command status */
     1.6  
     1.7 -  object Status
     1.8 -  {
     1.9 -    val init = Status()
    1.10 -  }
    1.11 -
    1.12    sealed case class Status(
    1.13 -    private val touched: Boolean = false,
    1.14 -    private val accepted: Boolean = false,
    1.15 -    private val failed: Boolean = false,
    1.16 -    forks: Int = 0,
    1.17 -    runs: Int = 0)
    1.18 +    private val touched: Boolean,
    1.19 +    private val accepted: Boolean,
    1.20 +    private val failed: Boolean,
    1.21 +    forks: Int,
    1.22 +    runs: Int)
    1.23    {
    1.24      def + (that: Status): Status =
    1.25        Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    1.26 @@ -63,22 +58,25 @@
    1.27      def is_failed: Boolean = failed
    1.28    }
    1.29  
    1.30 -  def command_status(status: Status, markup: Markup): Status =
    1.31 -    markup match {
    1.32 -      case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
    1.33 -      case Markup(Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
    1.34 -      case Markup(Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.35 -      case Markup(Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
    1.36 -      case Markup(Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
    1.37 -      case Markup(Markup.FAILED, _) => status.copy(failed = true)
    1.38 -      case _ => status
    1.39 -    }
    1.40 -
    1.41 -  def command_status(status: Status, state: Command.State): Status =
    1.42 -    (status /: state.status)(command_status(_, _))
    1.43 -
    1.44 -  def command_status(status: Status, states: List[Command.State]): Status =
    1.45 -    (status /: states)(command_status(_, _))
    1.46 +  def command_status(markups: Iterator[Markup]): Status =
    1.47 +  {
    1.48 +    var touched = false
    1.49 +    var accepted = false
    1.50 +    var failed = false
    1.51 +    var forks = 0
    1.52 +    var runs = 0
    1.53 +    for { markup <- markups; name = markup.name }
    1.54 +      name match {
    1.55 +        case Markup.ACCEPTED => accepted = true
    1.56 +        case Markup.FORKED => touched = true; forks += 1
    1.57 +        case Markup.JOINED => forks -= 1
    1.58 +        case Markup.RUNNING => touched = true; runs += 1
    1.59 +        case Markup.FINISHED => runs -= 1
    1.60 +        case Markup.FAILED => failed = true
    1.61 +        case _ =>
    1.62 +      }
    1.63 +    Status(touched, accepted, failed, forks, runs)
    1.64 +  }
    1.65  
    1.66    val command_status_elements =
    1.67      Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    1.68 @@ -123,7 +121,7 @@
    1.69      for {
    1.70        command <- node.commands
    1.71        states = state.command_states(version, command)
    1.72 -      status = command_status(Status.init, states)
    1.73 +      status = command_status(states.iterator.flatMap(st => st.status.iterator))
    1.74      } {
    1.75        if (status.is_running) running += 1
    1.76        else if (status.is_finished) {