src/Pure/PIDE/protocol.scala
changeset 49036 4680c4046814
parent 49009 15381ea111ec
child 49039 e780d1bf767e
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Aug 30 22:38:12 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Aug 31 13:23:25 2012 +0200
     1.3 @@ -49,32 +49,34 @@
     1.4    }
     1.5  
     1.6    sealed case class Status(
     1.7 +    private val touched: Boolean = false,
     1.8      private val accepted: Boolean = false,
     1.9 -    private val finished: Boolean = false,
    1.10      private val failed: Boolean = false,
    1.11 -    forks: Int = 0)
    1.12 +    forks: Int = 0,
    1.13 +    runs: Int = 0)
    1.14    {
    1.15 -    def is_unprocessed: Boolean = accepted && !finished && !failed && forks == 0
    1.16 -    def is_running: Boolean = forks != 0
    1.17 -    def is_finished: Boolean = finished && forks == 0
    1.18 -    def is_failed: Boolean = failed && forks == 0
    1.19      def + (that: Status): Status =
    1.20 -      Status(accepted || that.accepted, finished || that.finished,
    1.21 -        failed || that.failed, forks + that.forks)
    1.22 +      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    1.23 +        forks + that.forks, runs + that.runs)
    1.24 +
    1.25 +    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    1.26 +    def is_running: Boolean = runs != 0
    1.27 +    def is_finished: Boolean = !failed && forks == 0 && runs == 0
    1.28 +    def is_failed: Boolean = failed
    1.29    }
    1.30  
    1.31    val command_status_markup: Set[String] =
    1.32 -    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    1.33 -      Isabelle_Markup.FORKED, Isabelle_Markup.JOINED, Isabelle_Markup.CANCELLED)
    1.34 +    Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FORKED, Isabelle_Markup.JOINED,
    1.35 +      Isabelle_Markup.RUNNING, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED)
    1.36  
    1.37    def command_status(status: Status, markup: Markup): Status =
    1.38      markup match {
    1.39        case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
    1.40 -      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
    1.41 +      case Markup(Isabelle_Markup.FORKED, _) => status.copy(touched = true, forks = status.forks + 1)
    1.42 +      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.43 +      case Markup(Isabelle_Markup.RUNNING, _) => status.copy(touched = true, runs = status.runs + 1)
    1.44 +      case Markup(Isabelle_Markup.FINISHED, _) => status.copy(runs = status.runs - 1)
    1.45        case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    1.46 -      case Markup(Isabelle_Markup.CANCELLED, _) => status.copy(failed = true)
    1.47 -      case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
    1.48 -      case Markup(Isabelle_Markup.JOINED, _) => status.copy(forks = status.forks - 1)
    1.49        case _ => status
    1.50      }
    1.51