clarified messages (amending 3e072441c96a);
authorwenzelm
Sat, 24 Mar 2018 22:10:14 +0100
changeset 67947 ad735a551a11
parent 67946 e1e57c288e45
child 67948 83902fff6243
clarified messages (amending 3e072441c96a);
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)
     }