src/Pure/PIDE/document_id.scala

--- a/src/Pure/PIDE/document_id.scala	Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/PIDE/document_id.scala	Mon Jul 01 12:40:54 2024 +0200
@@ -20,4 +20,6 @@
 
   def apply(id: Generic): String = Value.Long.apply(id)
   def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
+
+  def encode(id: Generic): XML.Body = XML.Encode.long(id)
 }