# HG changeset patch
# User wenzelm
# Date 1521733162 -3600
# Node ID 3e072441c96af78db58641784c96382a2a8e53d2
# Parent  9e668ae81f97700ac5d03264b29ba70b3ef1eae3
clarified exported messages, e.g. suppress "information", "tracing";
export "legacy_feature" as "warning", in accordance to console default output;

diff -r 9e668ae81f97 -r 3e072441c96a src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Thu Mar 22 16:20:53 2018 +0100
+++ b/src/Doc/System/Server.thy	Thu Mar 22 16:39:22 2018 +0100
@@ -468,9 +468,8 @@
 
   \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
   the \<open>kind\<close> provides some hint about the role and importance of the message.
-  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>, and
-  \<^verbatim>\<open>error\<close>. The table \<^verbatim>\<open>Markup.messages\<close> in Isabelle/Scala defines further
-  message kinds for more specific applications.
+  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>,
+  \<^verbatim>\<open>error\<close>. Messages without explicit kind can be treated like \<^verbatim>\<open>writeln\<close>.
 
   \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
   error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
diff -r 9e668ae81f97 -r 3e072441c96a src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:20:53 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:39:22 2018 +0100
@@ -239,6 +239,13 @@
       case _ => false
     }
 
+  def is_writeln(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.WRITELN, _), _) => true
+      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
+      case _ => false
+    }
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -263,6 +270,9 @@
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
+  def is_exported(msg: XML.Tree): Boolean =
+    is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
+
 
   /* breakpoints */
 
diff -r 9e668ae81f97 -r 3e072441c96a src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Thu Mar 22 16:20:53 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Thu Mar 22 16:39:22 2018 +0100
@@ -65,7 +65,6 @@
           Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
         pos = command.span.keyword_pos(start).position(command.span.name)
         (_, tree) <- state.command_results(version, command).iterator
-        if Protocol.is_inlined(tree)
        } yield (tree, pos)).toList
     }
   }
diff -r 9e668ae81f97 -r 3e072441c96a src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:20:53 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:39:22 2018 +0100
@@ -199,7 +199,9 @@
           case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
           case elem: XML.Elem =>
             val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
-            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
+            val kind =
+              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
+                if (Protocol.is_legacy(elem)) Markup.WARNING else a })
             Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
         }
       }
@@ -211,6 +213,7 @@
             (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