tuned;
authorwenzelm
Wed Mar 21 21:31:16 2018 +0100 (14 months ago)
changeset 67915d827728b74b3
parent 67914 9f82f6cc3bfc
child 67916 a72f01c63262
tuned;
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 21 19:26:50 2018 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Mar 21 21:31:16 2018 +0100
     1.3 @@ -144,13 +144,13 @@
     1.4    sealed case class Node_Status(
     1.5      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     1.6    {
     1.7 +    def ok: Boolean = failed == 0
     1.8      def total: Int = unprocessed + running + warned + failed + finished
     1.9 -    def ok: Boolean = failed == 0
    1.10  
    1.11      def json: JSON.Object.T =
    1.12 -      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
    1.13 -        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
    1.14 -        "total" -> total, "ok" -> ok)
    1.15 +      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    1.16 +        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    1.17 +        "consolidated" -> consolidated)
    1.18    }
    1.19  
    1.20    def node_status(