src/Pure/Tools/server_commands.scala
changeset 67912 a7731d581bbc
parent 67901 3e6864cf387f
child 67914 9f82f6cc3bfc
     1.1 --- a/src/Pure/Tools/server_commands.scala	Wed Mar 21 13:17:30 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Wed Mar 21 17:55:17 2018 +0100
     1.3 @@ -89,14 +89,19 @@
     1.4  
     1.5        val results_json =
     1.6          JSON.Object(
     1.7 +          "ok" -> results.ok,
     1.8            "return_code" -> results.rc,
     1.9            "sessions" ->
    1.10              results.sessions.toList.sortBy(sessions_order).map(session =>
    1.11 -              JSON.Object(
    1.12 -                "session" -> session,
    1.13 -                "return_code" -> results(session).rc,
    1.14 -                "timeout" -> results(session).timeout,
    1.15 -                "timing" -> results(session).timing.json)))
    1.16 +              {
    1.17 +                val result = results(session)
    1.18 +                JSON.Object(
    1.19 +                  "session" -> session,
    1.20 +                  "ok" -> result.ok,
    1.21 +                  "return_code" -> result.rc,
    1.22 +                  "timeout" -> result.timeout,
    1.23 +                  "timing" -> result.timing.json)
    1.24 +              }))
    1.25  
    1.26        if (results.ok) (results_json, results, base_info)
    1.27        else throw new Server.Error("Session build failed: return code " + results.rc, results_json)