# HG changeset patch
# User wenzelm
# Date 1671375697 -3600
# Node ID e95b9c9e17ff7ad8b7db57b5c4a2a81ca979a49c
# Parent  fdaa17402af32d97779d3fef23f7af1de8ede6a7
clarified signature;

diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Dec 18 15:50:51 2022 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Dec 18 16:01:37 2022 +0100
@@ -340,7 +340,7 @@
           props match {
             case Markup.Serial(i) =>
               val markup_message =
-                cache.elem(Protocol.make_message(body, kind = name, props = props))
+                cache.elem(Protocol.make_message(body, name, props = props))
               val message_markup =
                 cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
 
diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Dec 18 15:50:51 2022 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Dec 18 16:01:37 2022 +0100
@@ -202,13 +202,16 @@
     text1 + text2
   }
 
-  def make_message(body: XML.Body,
-    kind: String = Markup.WRITELN,
-    props: Properties.T = Nil
-  ): XML.Elem = XML.Elem(Markup(Markup.message(kind), props), body)
+  def make_message(body: XML.Body, kind: String, props: Properties.T = Nil): XML.Elem =
+    XML.Elem(Markup(Markup.message(kind), props), body)
 
-  def warning_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.WARNING)
-  def error_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.ERROR)
+  def writeln_message(body: XML.Body): XML.Elem = make_message(body, Markup.WRITELN)
+  def warning_message(body: XML.Body): XML.Elem = make_message(body, Markup.WARNING)
+  def error_message(body: XML.Body): XML.Elem = make_message(body, Markup.ERROR)
+
+  def writeln_message(msg: String): XML.Elem = writeln_message(XML.string(msg))
+  def warning_message(msg: String): XML.Elem = warning_message(XML.string(msg))
+  def error_message(msg: String): XML.Elem = error_message(XML.string(msg))
 
 
   /* ML profiling */
diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Sun Dec 18 15:50:51 2022 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Sun Dec 18 16:01:37 2022 +0100
@@ -119,7 +119,7 @@
         XML.Elem(_, List(XML.Elem(markup, body))) <- results
         if Markup.messages.contains(markup.name)
         body1 = resolve_sendback(body)
-      } yield Protocol.make_message(body1, kind = markup.name, props = markup.properties)
+      } yield Protocol.make_message(body1, markup.name, props = markup.properties)
 
 
     /* status */
diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sun Dec 18 15:50:51 2022 +0100
+++ b/src/Pure/Tools/debugger.scala	Sun Dec 18 16:01:37 2022 +0100
@@ -123,7 +123,7 @@
         case Markup.Debugger_Output(thread_name) =>
           Symbol.decode_yxml_failsafe(msg.text) match {
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
-              val message = Protocol.make_message(body, kind = name, props = props)
+              val message = Protocol.make_message(body, name, props = props)
               debugger.add_output(thread_name, i -> session.cache.elem(message))
               true
             case _ => false
diff -r fdaa17402af3 -r e95b9c9e17ff src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sun Dec 18 15:50:51 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Sun Dec 18 16:01:37 2022 +0100
@@ -142,8 +142,8 @@
               }
             val msg =
               res match {
-                case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
-                case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
+                case Exn.Res(_) => Protocol.writeln_message("OK")
+                case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
               }
             val result = Document_Dockable.Result(output = List(msg))
             current_state.change(_ => Document_Dockable.State.finish(result))