clarified messages (amending 3e072441c96a);
authorwenzelm
Sat Mar 24 22:10:14 2018 +0100 (13 months ago)
changeset 67947ad735a551a11
parent 67946 e1e57c288e45
child 67948 83902fff6243
clarified messages (amending 3e072441c96a);
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Tools/server_commands.scala	Sat Mar 24 21:14:49 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Sat Mar 24 22:10:14 2018 +0100
     1.3 @@ -204,15 +204,15 @@
     1.4              (for {
     1.5                (name, status) <- result.nodes if !status.ok
     1.6                (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
     1.7 -              if Protocol.is_exported(tree)
     1.8              } yield output_message(tree, pos)),
     1.9            "nodes" ->
    1.10              (for ((name, status) <- result.nodes) yield
    1.11                name.json +
    1.12                  ("status" -> status.json) +
    1.13                  ("messages" ->
    1.14 -                  (for ((tree, pos) <- result.messages(name))
    1.15 -                    yield output_message(tree, pos)))))
    1.16 +                  (for {
    1.17 +                    (tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
    1.18 +                  } yield output_message(tree, pos)))))
    1.19  
    1.20        (result_json, result)
    1.21      }