tuned;

--- a/src/Pure/General/symbol.scala	Fri Jun 28 13:14:15 2024 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 28 13:20:18 2024 +0200
@@ -265,11 +265,11 @@
       tab
     }
     def recode(text: String): String = {
-      val len = text.length
+      val n = text.length
       val matcher = new Symbol.Matcher(text)
-      Library.string_builder(hint = len) { result =>
+      Library.string_builder(hint = n) { result =>
         var i = 0
-        while (i < len) {
+        while (i < n) {
           val c = text(i)
           if (min <= c && c <= max) {
             val s = matcher.match_symbol(i)