src/Pure/PIDE/command_span.scala
changeset 65335 7634d33c1a79
parent 63606 fc3a23763617
child 65717 556c34fd0554
--- a/src/Pure/PIDE/command_span.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/PIDE/command_span.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -56,4 +56,30 @@
 
   def unparsed(source: String): Span =
     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+
+
+  /* XML data representation */
+
+  def encode: XML.Encode.T[Span] = (span: Span) =>
+  {
+    import XML.Encode._
+    val kind: T[Kind] =
+      variant(List(
+        { case Command_Span(a, b) => (List(a), properties(b)) },
+        { case Ignored_Span => (Nil, Nil) },
+        { case Malformed_Span => (Nil, Nil) }))
+    pair(kind, list(Token.encode))((span.kind, span.content))
+  }
+
+  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val kind: T[Kind] =
+      variant(List(
+        { case (List(a), b) => Command_Span(a, properties(b)) },
+        { case (Nil, Nil) => Ignored_Span },
+        { case (Nil, Nil) => Malformed_Span }))
+    val (k, toks) = pair(kind, list(Token.decode))(body)
+    Span(k, toks)
+  }
 }