--- a/src/Pure/General/symbol.scala Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/symbol.scala Tue Jul 02 23:13:35 2024 +0200
@@ -541,10 +541,10 @@
def encode(text: String): String = symbols.encode(text)
def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
- YXML.parse_body(text, recode = decode, cache = cache)
+ YXML.parse_body(YXML.Source(text), recode = decode, cache = cache)
def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
- YXML.parse_body_failsafe(text, recode = decode, cache = cache)
+ YXML.parse_body_failsafe(YXML.Source(text), recode = decode, cache = cache)
def encode_yxml(body: XML.Body): String =
YXML.string_of_body(body, recode = encode)