# HG changeset patch
# User wenzelm
# Date 1719523661 -7200
# Node ID b42f95f18a714b28b6a8bfa6aa1675d9f4e165c4
# Parent  c748adebc67fab275e432c25abe93945b297b330
tuned;

diff -r c748adebc67f -r b42f95f18a71 src/Pure/PIDE/xml.scala
--- 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
         }
       }
     }