# 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) }