src/Pure/PIDE/protocol.scala
changeset 56395 0546e036d1c0
parent 56387 d92eb5c3960d
child 56447 1e77ed11f2f7
     1.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:08:00 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:55:48 2014 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4      {
     1.5        var touched = false
     1.6        var accepted = false
     1.7 +      var warned = false
     1.8        var failed = false
     1.9        var forks = 0
    1.10        var runs = 0
    1.11 @@ -57,11 +58,12 @@
    1.12            case Markup.JOINED => forks -= 1
    1.13            case Markup.RUNNING => touched = true; runs += 1
    1.14            case Markup.FINISHED => runs -= 1
    1.15 -          case Markup.FAILED => failed = true
    1.16 +          case Markup.WARNING => warned = true
    1.17 +          case Markup.FAILED | Markup.ERROR => failed = true
    1.18            case _ =>
    1.19          }
    1.20        }
    1.21 -      Status(touched, accepted, failed, forks, runs)
    1.22 +      Status(touched, accepted, warned, failed, forks, runs)
    1.23      }
    1.24  
    1.25      val empty = make(Iterator.empty)
    1.26 @@ -77,26 +79,33 @@
    1.27    sealed case class Status(
    1.28      private val touched: Boolean,
    1.29      private val accepted: Boolean,
    1.30 +    private val warned: Boolean,
    1.31      private val failed: Boolean,
    1.32      forks: Int,
    1.33      runs: Int)
    1.34    {
    1.35      def + (that: Status): Status =
    1.36 -      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
    1.37 -        forks + that.forks, runs + that.runs)
    1.38 +      Status(
    1.39 +        touched || that.touched,
    1.40 +        accepted || that.accepted,
    1.41 +        warned || that.warned,
    1.42 +        failed || that.failed,
    1.43 +        forks + that.forks,
    1.44 +        runs + that.runs)
    1.45  
    1.46      def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    1.47      def is_running: Boolean = runs != 0
    1.48      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    1.49 +    def is_warned: Boolean = is_finished && warned
    1.50      def is_failed: Boolean = failed
    1.51    }
    1.52  
    1.53 -  val command_status_elements =
    1.54 +  val proper_status_elements =
    1.55      Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
    1.56        Markup.FINISHED, Markup.FAILED)
    1.57  
    1.58 -  val status_elements =
    1.59 -    command_status_elements + Markup.WARNING + Markup.ERROR
    1.60 +  val liberal_status_elements =
    1.61 +    proper_status_elements + Markup.WARNING + Markup.ERROR
    1.62  
    1.63  
    1.64    /* command timing */
    1.65 @@ -136,10 +145,8 @@
    1.66        val status = Status.merge(states.iterator.map(_.protocol_status))
    1.67  
    1.68        if (status.is_running) running += 1
    1.69 -      else if (status.is_finished) {
    1.70 -        val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
    1.71 -        if (warning) warned += 1 else finished += 1
    1.72 -      }
    1.73 +      else if (status.is_warned) warned += 1
    1.74 +      else if (status.is_finished) finished += 1
    1.75        else if (status.is_failed) failed += 1
    1.76        else unprocessed += 1
    1.77      }