# HG changeset patch
# User wenzelm
# Date 1731405894 -3600
# Node ID d23d9fd83ef062d33a8aa7486d974bc0571d2101
# Parent  0ccfc82fff57d2169498d612282b8289cca386cf
tuned;

diff -r 0ccfc82fff57 -r d23d9fd83ef0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Nov 11 13:15:55 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Nov 12 11:04:54 2024 +0100
@@ -333,10 +333,8 @@
         case XML.Elem(Markup(name, props), body) =>
           props match {
             case Markup.Serial(i) =>
-              val markup_message =
-                cache.elem(Protocol.make_message(body, name, props = props))
-              val message_markup =
-                cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
+              val markup_message = cache.elem(Protocol.make_message(body, name, props = props))
+              val message_markup = cache.elem(XML.elem(Markup(name, Markup.Serial(i))))
 
               var st = add_result(i -> markup_message)
               if (Protocol.is_inlined(message)) {