src/Pure/PIDE/protocol.scala
changeset 46910 3e068ef04b42
parent 46812 3d55ef732cd7
child 46938 cda018294515
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 13 20:04:24 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 13 21:17:37 2012 +0100
     1.3 @@ -49,24 +49,27 @@
     1.4    }
     1.5  
     1.6    sealed case class Status(
     1.7 +    private val parsed: Boolean = false,
     1.8      private val finished: Boolean = false,
     1.9      private val failed: Boolean = false,
    1.10      forks: Int = 0)
    1.11    {
    1.12 -    def is_unprocessed: Boolean = !finished && !failed && forks == 0
    1.13 +    def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0
    1.14      def is_running: Boolean = forks != 0
    1.15      def is_finished: Boolean = finished && forks == 0
    1.16      def is_failed: Boolean = failed && forks == 0
    1.17      def + (that: Status): Status =
    1.18 -      Status(finished || that.finished, failed || that.failed, forks + that.forks)
    1.19 +      Status(parsed || that.parsed, finished || that.finished,
    1.20 +        failed || that.failed, forks + that.forks)
    1.21    }
    1.22  
    1.23    val command_status_markup: Set[String] =
    1.24 -    Set(Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    1.25 +    Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
    1.26        Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
    1.27  
    1.28    def command_status(status: Status, markup: Markup): Status =
    1.29      markup match {
    1.30 +      case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true)
    1.31        case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
    1.32        case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
    1.33        case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)