src/Pure/PIDE/yxml.scala

--- a/src/Pure/PIDE/yxml.scala	Fri Jun 28 15:59:45 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Fri Jun 28 16:51:55 2024 +0200
@@ -93,11 +93,19 @@
     if (name == "") err("unbalanced element")
     else err("unbalanced element " + quote(name))
 
-  private def parse_attrib(source: CharSequence): (String, String) =
-    Properties.Eq.unapply(source.toString) getOrElse err_attribute()
+  def parse_body(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Body = {
+    /* parse + recode */
+
+    def parse_string(s: CharSequence): String = recode(s.toString)
+
+    def parse_attrib(s: CharSequence): (String, String) =
+      Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute()
 
 
-  def parse_body(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
@@ -126,8 +134,9 @@
       else {
         Library.separated_chunks(is_Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
-            push(name.toString, atts.map(parse_attrib))
-          case txts => for (txt <- txts) add(cache.tree0(XML.Text(cache.string(txt.toString))))
+            push(parse_string(name), atts.map(parse_attrib))
+          case txts =>
+            for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
         }
       }
     }
@@ -137,15 +146,23 @@
     }
   }
 
-  def parse(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
-    parse_body(source, cache = cache) match {
+  def parse(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree =
+    parse_body(source, recode = recode, cache = cache) match {
       case List(result) => result
       case Nil => XML.no_text
       case _ => err("multiple XML trees")
     }
 
-  def parse_elem(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree =
-    parse_body(source, cache = cache) match {
+  def parse_elem(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree =
+    parse_body(source, recode = recode, cache = cache) match {
       case List(elem: XML.Elem) => elem
       case _ => err("single XML element expected")
     }
@@ -156,13 +173,21 @@
   private def markup_broken(source: CharSequence) =
     XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
-  def parse_body_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Body = {
-    try { parse_body(source, cache = cache) }
+  def parse_body_failsafe(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Body = {
+    try { parse_body(source, recode = recode, cache = cache) }
     catch { case ERROR(_) => List(markup_broken(source)) }
   }
 
-  def parse_failsafe(source: CharSequence, cache: XML.Cache = XML.Cache.none): XML.Tree = {
-    try { parse(source, cache = cache) }
+  def parse_failsafe(
+    source: CharSequence,
+    recode: String => String = identity,
+    cache: XML.Cache = XML.Cache.none
+  ): XML.Tree = {
+    try { parse(source, recode = recode, cache = cache) }
     catch { case ERROR(_) => markup_broken(source) }
   }
 }