--- a/src/Pure/General/symbol.scala Fri Jun 28 15:59:45 2024 +0200
+++ b/src/Pure/General/symbol.scala Fri Jun 28 16:51:55 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(decode(text), cache = cache)
+ YXML.parse_body(text, recode = decode, cache = cache)
def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
- YXML.parse_body_failsafe(decode(text), cache = cache)
+ YXML.parse_body_failsafe(text, recode = decode, cache = cache)
def encode_yxml(body: XML.Body): String =
YXML.string_of_body(body, recode = encode)