# HG changeset patch
# User wenzelm
# Date 1521369777 -3600
# Node ID 5a1b0076d7f05577d7cf1379dd47c2252a908d0f
# Parent  730fa992da38447dcea42acf9676599355d8d191
more explicit errors;
tuned;

diff -r 730fa992da38 -r 5a1b0076d7f0 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Mar 17 18:51:56 2018 +1100
+++ b/src/Pure/Tools/server_commands.scala	Sun Mar 18 11:42:57 2018 +0100
@@ -206,14 +206,20 @@
       val result_json =
         JSON.Object(
           "ok" -> result.ok,
+          "errors" ->
+            (for {
+              (name, status) <- result.nodes if !status.ok
+              (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
+            } yield output_message(tree, pos)),
           "nodes" ->
-            (for ((name, st) <- result.nodes) yield
+            (for ((name, status) <- result.nodes) yield
               JSON.Object(
                 "node_name" -> name.node,
                 "theory" -> name.theory,
-                "status" -> st.json,
+                "status" -> status.json,
                 "messages" ->
-                  (for ((tree, pos) <- result.messages(name)) yield output_message(tree, pos)))))
+                  (for ((tree, pos) <- result.messages(name))
+                    yield output_message(tree, pos)))))
 
       (result_json, result)
     }