clarified exported messages, e.g. suppress "information", "tracing";
authorwenzelm
Thu Mar 22 16:39:22 2018 +0100 (16 months ago)
changeset 679233e072441c96a
parent 67922 9e668ae81f97
child 67924 b2cdd24e83b6
clarified exported messages, e.g. suppress "information", "tracing";
export "legacy_feature" as "warning", in accordance to console default output;
src/Doc/System/Server.thy
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 16:20:53 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 16:39:22 2018 +0100
     1.3 @@ -468,9 +468,8 @@
     1.4  
     1.5    \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
     1.6    the \<open>kind\<close> provides some hint about the role and importance of the message.
     1.7 -  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>, and
     1.8 -  \<^verbatim>\<open>error\<close>. The table \<^verbatim>\<open>Markup.messages\<close> in Isabelle/Scala defines further
     1.9 -  message kinds for more specific applications.
    1.10 +  The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>,
    1.11 +  \<^verbatim>\<open>error\<close>. Messages without explicit kind can be treated like \<^verbatim>\<open>writeln\<close>.
    1.12  
    1.13    \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
    1.14    error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
     2.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:20:53 2018 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 22 16:39:22 2018 +0100
     2.3 @@ -239,6 +239,13 @@
     2.4        case _ => false
     2.5      }
     2.6  
     2.7 +  def is_writeln(msg: XML.Tree): Boolean =
     2.8 +    msg match {
     2.9 +      case XML.Elem(Markup(Markup.WRITELN, _), _) => true
    2.10 +      case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
    2.11 +      case _ => false
    2.12 +    }
    2.13 +
    2.14    def is_warning(msg: XML.Tree): Boolean =
    2.15      msg match {
    2.16        case XML.Elem(Markup(Markup.WARNING, _), _) => true
    2.17 @@ -263,6 +270,9 @@
    2.18    def is_inlined(msg: XML.Tree): Boolean =
    2.19      !(is_result(msg) || is_tracing(msg) || is_state(msg))
    2.20  
    2.21 +  def is_exported(msg: XML.Tree): Boolean =
    2.22 +    is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
    2.23 +
    2.24  
    2.25    /* breakpoints */
    2.26  
     3.1 --- a/src/Pure/Thy/thy_resources.scala	Thu Mar 22 16:20:53 2018 +0100
     3.2 +++ b/src/Pure/Thy/thy_resources.scala	Thu Mar 22 16:39:22 2018 +0100
     3.3 @@ -65,7 +65,6 @@
     3.4            Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
     3.5          pos = command.span.keyword_pos(start).position(command.span.name)
     3.6          (_, tree) <- state.command_results(version, command).iterator
     3.7 -        if Protocol.is_inlined(tree)
     3.8         } yield (tree, pos)).toList
     3.9      }
    3.10    }
     4.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:20:53 2018 +0100
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 16:39:22 2018 +0100
     4.3 @@ -199,7 +199,9 @@
     4.4            case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
     4.5            case elem: XML.Elem =>
     4.6              val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
     4.7 -            val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
     4.8 +            val kind =
     4.9 +              Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
    4.10 +                if (Protocol.is_legacy(elem)) Markup.WARNING else a })
    4.11              Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
    4.12          }
    4.13        }
    4.14 @@ -211,6 +213,7 @@
    4.15              (for {
    4.16                (name, status) <- result.nodes if !status.ok
    4.17                (tree, pos) <- result.messages(name) if Protocol.is_error(tree)
    4.18 +              if Protocol.is_exported(tree)
    4.19              } yield output_message(tree, pos)),
    4.20            "nodes" ->
    4.21              (for ((name, status) <- result.nodes) yield