--- a/src/Pure/GUI/rich_text.scala Sun Nov 10 12:23:41 2024 +0100
+++ b/src/Pure/GUI/rich_text.scala Sun Nov 10 12:29:32 2024 +0100
@@ -35,7 +35,7 @@
result += command(body = Pretty.Separator, id = Document_ID.make())
}
val body = Pretty.formatted(List(msg), margin = margin, metric = metric)
- result += command(body = body, id = Markup.Serial.get(msg.markup.properties))
+ result += command(body = body, id = Protocol_Message.get_serial(msg))
Exn.Interrupt.expose()
}
--- 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())))