more informative JSON results;
authorwenzelm
Wed, 14 Mar 2018 17:43:30 +0100
changeset 67858 cba5c5657378
parent 67857 262d62a4c32b
child 67859 612846bff1ea
more informative JSON results;
src/Pure/General/timing.scala
src/Pure/Tools/server_commands.scala
--- a/src/Pure/General/timing.scala	Wed Mar 14 16:52:16 2018 +0100
+++ b/src/Pure/General/timing.scala	Wed Mar 14 17:43:30 2018 +0100
@@ -70,4 +70,7 @@
   }
 
   override def toString: String = message
+
+  def json: JSON.Object.T =
+    JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds)
 }
--- a/src/Pure/Tools/server_commands.scala	Wed Mar 14 16:52:16 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Wed Mar 14 17:43:30 2018 +0100
@@ -42,7 +42,7 @@
           system_mode = system_mode, verbose = verbose)
       }
 
-    def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) =
+    def command(progress: Progress, args: Args): (JSON.T, Build.Results, Sessions.Base_Info) =
     {
       val options = Options.init(prefs = args.prefs, opts = args.opts)
       val dirs = args.dirs.map(Path.explode(_))
@@ -68,7 +68,23 @@
           verbose = args.verbose,
           sessions = List(args.session))
 
-      (JSON.Object("rc" -> results.rc), base_info, results)
+      val sessions_order =
+        base_info.sessions_structure.imports_topological_order.zipWithIndex.
+          toMap.withDefaultValue(-1)
+
+      val results_json =
+        JSON.Object(
+          "return_code" -> results.rc,
+          "sessions" ->
+            results.sessions.toList.sortBy(sessions_order).map(session =>
+              JSON.Object(
+                "session" -> session,
+                "return_code" -> results(session).rc,
+                "timeout" -> results(session).timeout,
+                "timing" -> results(session).timing.json)))
+
+      if (results.ok) (results_json, results, base_info)
+      else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
     }
   }
 }