src/Pure/General/symbol.scala
changeset 65344 b99283eed13c
parent 65335 7634d33c1a79
child 65521 e307a781416a
--- a/src/Pure/General/symbol.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/General/symbol.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -506,8 +506,9 @@
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
-  def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x)))
-  def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x)))
+  def decode_yxml(text: String): XML.Body = YXML.parse_body(decode(text))
+  def decode_yxml_failsafe(text: String): XML.Body = YXML.parse_body_failsafe(decode(text))
+  def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
 
   def decode_strict(text: String): String =
   {