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