src/Pure/PIDE/command.scala
changeset 76022 6ce62e4e7dc0
parent 75393 87ebf5a50283
child 76234 035ffcd82fb2
--- 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))))