--- 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))))
--- 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 */
--- 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 */
--- 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