tuned;

--- a/src/Pure/PIDE/xml.scala	Thu Jun 27 23:18:28 2024 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Jun 27 23:27:41 2024 +0200
@@ -157,15 +157,13 @@
     def string(str: String, permissive: Boolean = false): Unit = {
       if (str == null) { builder ++= str }
       else {
-        for (c <- str) {
-          c match {
-            case '<' => builder ++= "&lt;"
-            case '>' => builder ++= "&gt;"
-            case '&' => builder ++= "&amp;"
-            case '"' if !permissive => builder ++= "&quot;"
-            case '\'' if !permissive => builder ++= "&apos;"
-            case _ => builder += c
-          }
+        str foreach {
+          case '<' => builder ++= "&lt;"
+          case '>' => builder ++= "&gt;"
+          case '&' => builder ++= "&amp;"
+          case '"' if !permissive => builder ++= "&quot;"
+          case '\'' if !permissive => builder ++= "&apos;"
+          case c => builder += c
         }
       }
     }