# HG changeset patch
# User wenzelm
# Date 1521925814 -3600
# Node ID ad735a551a110115f079e3af9e27f4c3a764c61c
# Parent  e1e57c288e45cdfff068001ca517e51dd2389c50
clarified messages (amending 3e072441c96a);

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