src/Pure/PIDE/document_status.scala
changeset 68871 f5c76072db55
parent 68770 add44e2b8cb0
child 68873 13a984eba612
     1.1 --- a/src/Pure/PIDE/document_status.scala	Sat Sep 01 18:39:36 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Sat Sep 01 20:20:50 2018 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    {
     1.5      val proper_elements: Markup.Elements =
     1.6        Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     1.7 -        Markup.FINISHED, Markup.FAILED)
     1.8 +        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
     1.9  
    1.10      val liberal_elements: Markup.Elements =
    1.11        proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    1.12 @@ -26,6 +26,7 @@
    1.13        var accepted = false
    1.14        var warned = false
    1.15        var failed = false
    1.16 +      var canceled = false
    1.17        var forks = 0
    1.18        var runs = 0
    1.19        for (markup <- markup_iterator) {
    1.20 @@ -37,10 +38,11 @@
    1.21            case Markup.FINISHED => runs -= 1
    1.22            case Markup.WARNING | Markup.LEGACY => warned = true
    1.23            case Markup.FAILED | Markup.ERROR => failed = true
    1.24 +          case Markup.CANCELED => canceled = true
    1.25            case _ =>
    1.26          }
    1.27        }
    1.28 -      Command_Status(touched, accepted, warned, failed, forks, runs)
    1.29 +      Command_Status(touched, accepted, warned, failed, canceled, forks, runs)
    1.30      }
    1.31  
    1.32      val empty = make(Iterator.empty)
    1.33 @@ -58,6 +60,7 @@
    1.34      private val accepted: Boolean,
    1.35      private val warned: Boolean,
    1.36      private val failed: Boolean,
    1.37 +    private val canceled: Boolean,
    1.38      forks: Int,
    1.39      runs: Int)
    1.40    {
    1.41 @@ -67,6 +70,7 @@
    1.42          accepted || that.accepted,
    1.43          warned || that.warned,
    1.44          failed || that.failed,
    1.45 +        canceled || that.canceled,
    1.46          forks + that.forks,
    1.47          runs + that.runs)
    1.48  
    1.49 @@ -75,6 +79,7 @@
    1.50      def is_warned: Boolean = warned
    1.51      def is_failed: Boolean = failed
    1.52      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    1.53 +    def is_canceled: Boolean = canceled
    1.54    }
    1.55  
    1.56  
    1.57 @@ -94,6 +99,7 @@
    1.58        var warned = 0
    1.59        var failed = 0
    1.60        var finished = 0
    1.61 +      var canceled = false
    1.62        for (command <- node.commands.iterator) {
    1.63          val states = state.command_states(version, command)
    1.64          val status = Command_Status.merge(states.iterator.map(_.document_status))
    1.65 @@ -103,17 +109,20 @@
    1.66          else if (status.is_warned) warned += 1
    1.67          else if (status.is_finished) finished += 1
    1.68          else unprocessed += 1
    1.69 +
    1.70 +        if (status.is_canceled) canceled = true
    1.71        }
    1.72        val initialized = state.node_initialized(version, name)
    1.73        val consolidated = state.node_consolidated(version, name)
    1.74  
    1.75 -      Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
    1.76 +      Node_Status(
    1.77 +        unprocessed, running, warned, failed, finished, canceled, initialized, consolidated)
    1.78      }
    1.79    }
    1.80  
    1.81    sealed case class Node_Status(
    1.82      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
    1.83 -    initialized: Boolean, consolidated: Boolean)
    1.84 +    canceled: Boolean, initialized: Boolean, consolidated: Boolean)
    1.85    {
    1.86      def ok: Boolean = failed == 0
    1.87      def total: Int = unprocessed + running + warned + failed + finished
    1.88 @@ -121,7 +130,7 @@
    1.89      def json: JSON.Object.T =
    1.90        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    1.91          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    1.92 -        "initialized" -> initialized, "consolidated" -> consolidated)
    1.93 +        "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated)
    1.94    }
    1.95  
    1.96