src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Sat Jan 02 16:39:07 2021 +0100
+++ b/src/Pure/General/symbol.scala	Sat Jan 02 20:56:08 2021 +0100
@@ -521,8 +521,12 @@
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
-  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 decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
+    YXML.parse_body(decode(text), cache = cache)
+
+  def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
+    YXML.parse_body_failsafe(decode(text), cache = cache)
+
   def encode_yxml(body: XML.Body): String = encode(YXML.string_of_body(body))
 
   def decode_strict(text: String): String =