# HG changeset patch
# User wenzelm
# Date 1521810290 -3600
# Node ID f7917c15b566c8b415da783af66a316b3f83c3d0
# Parent  7dff1186daf376a4236d8d9db45288524091ea4b
field "kind" is always present, with default "writeln";

diff -r 7dff1186daf3 -r f7917c15b566 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Mar 23 11:39:41 2018 +0100
+++ b/src/Doc/System/Server.thy	Fri Mar 23 14:04:50 2018 +0100
@@ -466,10 +466,10 @@
   of command transactions in the Isabelle/PIDE protocol: it normally does not
   occur in externalized positions.
 
-  \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
+  \<^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>,
-  \<^verbatim>\<open>error\<close>. Messages without explicit kind can be treated like \<^verbatim>\<open>writeln\<close>.
+  \<^verbatim>\<open>error\<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
@@ -981,7 +981,7 @@
   \<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
 
   \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
-  (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
+  (with kind \<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>).
 \<close>
 
 
diff -r 7dff1186daf3 -r f7917c15b566 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 23 11:39:41 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 23 14:04:50 2018 +0100
@@ -127,8 +127,7 @@
     val OK, ERROR, FINISHED, FAILED, NOTE = Value
 
     def message(msg: String, kind: String = ""): JSON.Object.T =
-      if (kind == "") JSON.Object("message" -> msg)
-      else JSON.Object(Markup.KIND -> kind, "message" -> msg)
+      JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
 
     def error_message(msg: String): JSON.Object.T =
       message(msg, kind = Markup.ERROR)
diff -r 7dff1186daf3 -r f7917c15b566 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 11:39:41 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 14:04:50 2018 +0100
@@ -206,8 +206,8 @@
             val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
             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
+                if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse ""
+            Server.Reply.message(output_text(msg), kind = kind) + position
         }
       }