field "kind" is always present, with default "writeln";
authorwenzelm
Fri Mar 23 14:04:50 2018 +0100 (15 months ago)
changeset 67931f7917c15b566
parent 67930 7dff1186daf3
child 67932 04352338f7f3
field "kind" is always present, with default "writeln";
src/Doc/System/Server.thy
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 11:39:41 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 14:04:50 2018 +0100
     1.3 @@ -466,10 +466,10 @@
     1.4    of command transactions in the Isabelle/PIDE protocol: it normally does not
     1.5    occur in externalized positions.
     1.6  
     1.7 -  \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
     1.8 +  \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind: string, message: string, pos?: position}\<close> where
     1.9    the \<open>kind\<close> provides some hint about the role and importance of the message.
    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 +  \<^verbatim>\<open>error\<close>.
    1.13  
    1.14    \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
    1.15    error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
    1.16 @@ -981,7 +981,7 @@
    1.17    \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
    1.18  
    1.19    \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
    1.20 -  (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
    1.21 +  (with kind \<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>).
    1.22  \<close>
    1.23  
    1.24  
     2.1 --- a/src/Pure/Tools/server.scala	Fri Mar 23 11:39:41 2018 +0100
     2.2 +++ b/src/Pure/Tools/server.scala	Fri Mar 23 14:04:50 2018 +0100
     2.3 @@ -127,8 +127,7 @@
     2.4      val OK, ERROR, FINISHED, FAILED, NOTE = Value
     2.5  
     2.6      def message(msg: String, kind: String = ""): JSON.Object.T =
     2.7 -      if (kind == "") JSON.Object("message" -> msg)
     2.8 -      else JSON.Object(Markup.KIND -> kind, "message" -> msg)
     2.9 +      JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
    2.10  
    2.11      def error_message(msg: String): JSON.Object.T =
    2.12        message(msg, kind = Markup.ERROR)
     3.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 11:39:41 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 14:04:50 2018 +0100
     3.3 @@ -206,8 +206,8 @@
     3.4              val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
     3.5              val kind =
     3.6                Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
     3.7 -                if (Protocol.is_legacy(elem)) Markup.WARNING else a })
     3.8 -            Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
     3.9 +                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
    3.10 +            Server.Reply.message(output_text(msg), kind = kind) + position
    3.11          }
    3.12        }
    3.13