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