# HG changeset patch
# User wenzelm
# Date 1719573951 -7200
# Node ID 00f5e829d8b4420a0975e1526ef240f227fa8670
# Parent  2bbcfcfca0cd08af97590e1ac2562f61b8ac5301
minor performance tuning;

diff -r 2bbcfcfca0cd -r 00f5e829d8b4 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jun 28 13:46:06 2024 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 28 13:25:51 2024 +0200
@@ -266,19 +266,32 @@
     }
     def recode(text: String): String = {
       val n = text.length
-      val matcher = new Symbol.Matcher(text)
-      Library.string_builder(hint = n) { result =>
+      val relevant = {
         var i = 0
-        while (i < n) {
+        var found = false
+        while (i < n && !found) {
           val c = text(i)
-          if (min <= c && c <= max) {
-            val s = matcher.match_symbol(i)
-            result.append(table.getOrElse(s, s))
-            i += s.length
+          if (min <= c && c <= max) { found = true }
+          i += 1
+        }
+        found
+      }
+      if (relevant) {
+        val matcher = new Symbol.Matcher(text)
+        Library.string_builder(hint = n) { result =>
+          var i = 0
+          while (i < n) {
+            val c = text(i)
+            if (min <= c && c <= max) {
+              val s = matcher.match_symbol(i)
+              result.append(table.getOrElse(s, s))
+              i += s.length
+            }
+            else { result.append(c); i += 1 }
           }
-          else { result.append(c); i += 1 }
         }
       }
+      else text
     }
   }