src/Pure/PIDE/protocol.scala
changeset 46166 4beb2f41ed93
parent 46121 30a69cd8a9a0
child 46207 e76b77356ed6
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Jan 09 23:09:03 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Jan 09 23:11:28 2012 +0100
     1.3 @@ -43,24 +43,32 @@
     1.4  
     1.5    /* toplevel transactions */
     1.6  
     1.7 -  sealed abstract class Status
     1.8 -  case object Unprocessed extends Status
     1.9 -  case class Forked(forks: Int) extends Status
    1.10 -  case object Finished extends Status
    1.11 -  case object Failed extends Status
    1.12 -
    1.13 -  def command_status(markup: List[Markup]): Status =
    1.14 +  sealed case class Status(
    1.15 +    private val finished: Boolean = false,
    1.16 +    private val failed: Boolean = false,
    1.17 +    forks: Int = 0)
    1.18    {
    1.19 -    val forks = (0 /: markup) {
    1.20 -      case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1
    1.21 -      case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1
    1.22 -      case (i, _) => i
    1.23 +    def is_unprocessed: Boolean = !finished && !failed && forks == 0
    1.24 +    def is_running: Boolean = forks != 0
    1.25 +    def is_finished: Boolean = finished && forks == 0
    1.26 +    def is_failed: Boolean = failed && forks == 0
    1.27 +  }
    1.28 +
    1.29 +  val command_status_markup: Set[String] =
    1.30 +    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    1.31 +      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
    1.32 +
    1.33 +  def command_status(status: Status, markup: Markup): Status =
    1.34 +    markup match {
    1.35 +      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
    1.36 +      case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    1.37 +      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
    1.38 +      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.39 +      case _ => status
    1.40      }
    1.41 -    if (forks != 0) Forked(forks)
    1.42 -    else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed
    1.43 -    else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished
    1.44 -    else Unprocessed
    1.45 -  }
    1.46 +
    1.47 +  def command_status(markups: List[Markup]): Status =
    1.48 +    (Status() /: markups)(command_status(_, _))
    1.49  
    1.50    sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
    1.51    {
    1.52 @@ -75,11 +83,12 @@
    1.53      var finished = 0
    1.54      var failed = 0
    1.55      node.commands.foreach(command =>
    1.56 -      command_status(state.command_state(version, command).status) match {
    1.57 -        case Unprocessed => unprocessed += 1
    1.58 -        case Forked(_) => running += 1
    1.59 -        case Finished => finished += 1
    1.60 -        case Failed => failed += 1
    1.61 +      {
    1.62 +        val status = command_status(state.command_state(version, command).status)
    1.63 +        if (status.is_running) running += 1
    1.64 +        else if (status.is_finished) finished += 1
    1.65 +        else if (status.is_failed) failed += 1
    1.66 +        else unprocessed += 1
    1.67        })
    1.68      Node_Status(unprocessed, running, finished, failed)
    1.69    }