src/Pure/Isar/token.scala

--- a/src/Pure/Isar/token.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/Isar/token.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -218,6 +218,22 @@
 
   def reader(tokens: List[Token], start: Token.Pos): Reader =
     new Token_Reader(tokens, start)
+
+
+  /* XML data representation */
+
+  val encode: XML.Encode.T[Token] = (tok: Token) =>
+  {
+    import XML.Encode._
+    pair(int, string)(tok.kind.id, tok.source)
+  }
+
+  val decode: XML.Decode.T[Token] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val (k, s) = pair(int, string)(body)
+    Token(Kind(k), s)
+  }
 }