src/Pure/PIDE/markup.scala
changeset 65335 7634d33c1a79
parent 65317 b9f5cd845616
child 65753 787e5ee6ef53
--- a/src/Pure/PIDE/markup.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -607,6 +607,22 @@
         case _ => None
       }
   }
+
+
+  /* XML data representation */
+
+  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
+  {
+    import XML.Encode._
+    pair(string, properties)((markup.name, markup.properties))
+  }
+
+  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val (name, props) = pair(string, properties)(body)
+    Markup(name, props)
+  }
 }