# HG changeset patch
# User wenzelm
# Date 1521664276 -3600
# Node ID d827728b74b3399a608e8355db927dcce62b4bd3
# Parent  9f82f6cc3bfca53402e734d2dcee45f601ef8b3a
tuned;

diff -r 9f82f6cc3bfc -r d827728b74b3 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(