src/Pure/PIDE/markup.scala
changeset 65335 7634d33c1a79
parent 65317 b9f5cd845616
child 65753 787e5ee6ef53
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 20 17:24:40 2017 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Mar 20 20:43:26 2017 +0100
     1.3 @@ -607,6 +607,22 @@
     1.4          case _ => None
     1.5        }
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* XML data representation */
    1.10 +
    1.11 +  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
    1.12 +  {
    1.13 +    import XML.Encode._
    1.14 +    pair(string, properties)((markup.name, markup.properties))
    1.15 +  }
    1.16 +
    1.17 +  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
    1.18 +  {
    1.19 +    import XML.Decode._
    1.20 +    val (name, props) = pair(string, properties)(body)
    1.21 +    Markup(name, props)
    1.22 +  }
    1.23  }
    1.24  
    1.25