diff -r e1e57c288e45 -r ad735a551a11 src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Sat Mar 24 21:14:49 2018 +0100 +++ b/src/Pure/Tools/server_commands.scala Sat Mar 24 22:10:14 2018 +0100 @@ -204,15 +204,15 @@ (for { (name, status) <- result.nodes if !status.ok (tree, pos) <- result.messages(name) if Protocol.is_error(tree) - if Protocol.is_exported(tree) } yield output_message(tree, pos)), "nodes" -> (for ((name, status) <- result.nodes) yield name.json + ("status" -> status.json) + ("messages" -> - (for ((tree, pos) <- result.messages(name)) - yield output_message(tree, pos))))) + (for { + (tree, pos) <- result.messages(name) if Protocol.is_exported(tree) + } yield output_message(tree, pos))))) (result_json, result) }