tuned;
authorwenzelm
Wed, 21 Mar 2018 21:31:16 +0100
changeset 67915 d827728b74b3
parent 67914 9f82f6cc3bfc
child 67916 a72f01c63262
tuned;
src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Mar 21 19:26:50 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Mar 21 21:31:16 2018 +0100
@@ -144,13 +144,13 @@
   sealed case class Node_Status(
     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
   {
+    def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
-    def ok: Boolean = failed == 0
 
     def json: JSON.Object.T =
-      JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
-        "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
-        "total" -> total, "ok" -> ok)
+      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
+        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
+        "consolidated" -> consolidated)
   }
 
   def node_status(