more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
authorwenzelm
Tue Apr 08 21:48:09 2014 +0200 (2014-04-08)
changeset 564744df2727a0b5f
parent 56473 5b5c750e9763
child 56475 710dee42b3d0
more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 20:03:00 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 21:48:09 2014 +0200
     1.3 @@ -95,9 +95,9 @@
     1.4  
     1.5      def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     1.6      def is_running: Boolean = runs != 0
     1.7 +    def is_warned: Boolean = warned
     1.8 +    def is_failed: Boolean = failed
     1.9      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    1.10 -    def is_warned: Boolean = is_finished && warned
    1.11 -    def is_failed: Boolean = failed
    1.12    }
    1.13  
    1.14    val proper_status_elements =
    1.15 @@ -127,9 +127,9 @@
    1.16    /* node status */
    1.17  
    1.18    sealed case class Node_Status(
    1.19 -    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
    1.20 +    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
    1.21    {
    1.22 -    def total: Int = unprocessed + running + finished + warned + failed
    1.23 +    def total: Int = unprocessed + running + warned + failed + finished
    1.24    }
    1.25  
    1.26    def node_status(
    1.27 @@ -137,20 +137,20 @@
    1.28    {
    1.29      var unprocessed = 0
    1.30      var running = 0
    1.31 -    var finished = 0
    1.32      var warned = 0
    1.33      var failed = 0
    1.34 +    var finished = 0
    1.35      for (command <- node.commands.iterator) {
    1.36        val states = state.command_states(version, command)
    1.37        val status = Status.merge(states.iterator.map(_.protocol_status))
    1.38  
    1.39        if (status.is_running) running += 1
    1.40        else if (status.is_warned) warned += 1
    1.41 +      else if (status.is_failed) failed += 1
    1.42        else if (status.is_finished) finished += 1
    1.43 -      else if (status.is_failed) failed += 1
    1.44        else unprocessed += 1
    1.45      }
    1.46 -    Node_Status(unprocessed, running, finished, warned, failed)
    1.47 +    Node_Status(unprocessed, running, warned, failed, finished)
    1.48    }
    1.49  
    1.50