# HG changeset patch
# User wenzelm
# Date 1661951128 -7200
# Node ID 6ce62e4e7dc0b3ca46f4fcb88fede10c924cf96d
# Parent  752425c6957781a7c524f3918216b28e3a650eec
clarified signature;

diff -r 752425c69577 -r 6ce62e4e7dc0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 30 13:18:33 2022 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 31 15:05:28 2022 +0200
@@ -340,7 +340,7 @@
           props match {
             case Markup.Serial(i) =>
               val markup_message =
-                cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
+                cache.elem(Protocol.make_message(body, kind = name, props = props))
               val message_markup =
                 cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
 
diff -r 752425c69577 -r 6ce62e4e7dc0 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 30 13:18:33 2022 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Aug 31 15:05:28 2022 +0200
@@ -202,6 +202,14 @@
     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 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)
+
 
   /* ML profiling */
 
diff -r 752425c69577 -r 6ce62e4e7dc0 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Aug 30 13:18:33 2022 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Wed Aug 31 15:05:28 2022 +0200
@@ -119,7 +119,7 @@
         XML.Elem(_, List(XML.Elem(markup, body))) <- results
         if Markup.messages.contains(markup.name)
         body1 = resolve_sendback(body)
-      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
+      } yield Protocol.make_message(body1, kind = markup.name, props = markup.properties)
 
 
     /* status */
diff -r 752425c69577 -r 6ce62e4e7dc0 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 30 13:18:33 2022 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Aug 31 15:05:28 2022 +0200
@@ -124,7 +124,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 = XML.Elem(Markup(Markup.message(name), props), body)
+              val message = Protocol.make_message(body, kind = name, props = props)
               debugger.add_output(thread_name, i -> session.cache.elem(message))
               true
             case _ => false