# HG changeset patch
# User wenzelm
# Date 1717960527 -7200
# Node ID b48768f9567fc100ae3f5866cb1a0f764fd4cd76
# Parent  31df11a23d6efe72359648b7578dd7108a7e90b9
more operations, following Isabelle/ML;

diff -r 31df11a23d6e -r b48768f9567f src/Pure/thm_name.scala
--- a/src/Pure/thm_name.scala	Sun Jun 09 20:47:30 2024 +0200
+++ b/src/Pure/thm_name.scala	Sun Jun 09 21:15:27 2024 +0200
@@ -30,6 +30,20 @@
       case Thm_Name_Regex(name, Value.Nat(index)) => Thm_Name(name, index)
       case _ => Thm_Name(s, 0)
     }
+
+
+  /* XML data representation */
+
+  def encode: XML.Encode.T[Thm_Name] = { (thm_name: Thm_Name) =>
+    import XML.Encode._
+    pair(string, int)((thm_name.name, thm_name.index))
+  }
+
+  def decode: XML.Decode.T[Thm_Name] = { (body: XML.Body) =>
+    import XML.Decode._
+    val (name, index) = pair(string, int)(body)
+    Thm_Name(name, index)
+  }
 }
 
 sealed case class Thm_Name(name: String, index: Int) {