src/Pure/PIDE/protocol_message.scala

--- a/src/Pure/PIDE/protocol_message.scala	Sun Nov 10 12:23:41 2024 +0100
+++ b/src/Pure/PIDE/protocol_message.scala	Sun Nov 10 12:29:32 2024 +0100
@@ -36,8 +36,11 @@
 
   /* message serial */
 
+  def get_serial(msg: XML.Elem): Long =
+    Markup.Serial.get(msg.markup.properties)
+
   def provide_serial(msg: XML.Elem): XML.Elem =
-    if (Markup.Serial.get(msg.markup.properties) != 0L) msg
+    if (get_serial(msg) != 0L) msg
     else msg.copy(markup = msg.markup.update_properties(Markup.Serial(Document_ID.make())))