src/Pure/Tools/server_commands.scala
changeset 67923 3e072441c96a
parent 67922 9e668ae81f97
child 67925 74dce5658d4c
     1.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:20:53 2018 +0100
     1.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:39:22 2018 +0100
     1.3 @@ -199,7 +199,9 @@
     1.4            case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
     1.5            case elem: XML.Elem =>
     1.6              val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
     1.7 -            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
     1.8 +            val kind =
     1.9 +              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
    1.10 +                if (Protocol.is_legacy(elem)) Markup.WARNING else a })
    1.11              Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
    1.12          }
    1.13        }
    1.14 @@ -211,6 +213,7 @@
    1.15              (for {
    1.16                (name, status) <- result.nodes if !status.ok
    1.17                (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
    1.18 +              if Protocol.is_exported(tree)
    1.19              } yield output_message(tree, pos)),
    1.20            "nodes" ->
    1.21              (for ((name, status) <- result.nodes) yield