# HG changeset patch
# User wenzelm
# Date 1720013074 -7200
# Node ID dd2f5fb363a5c926edb8dd5bf9ba7cb3bab339af
# Parent  e0568c7b5bedba7cbfbca51c995776f8a6fbcfc8
tuned;

diff -r e0568c7b5bed -r dd2f5fb363a5 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Wed Jul 03 13:54:48 2024 +0200
+++ b/src/Pure/General/utf8.scala	Wed Jul 03 15:24:34 2024 +0200
@@ -17,17 +17,6 @@
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
-  def relevant(s: CharSequence): Boolean = {
-    var i = 0
-    val n = s.length
-    var found = false
-    while (i < n && !found) {
-      if (s.charAt(i) >= 128) { found = true }
-      i += 1
-    }
-    found
-  }
-
 
   /* permissive UTF-8 decoding */
 
@@ -72,7 +61,18 @@
     buf.toString
   }
 
-  def decode_permissive(text: String): String =
-    if (relevant(text)) decode_permissive_bytes(new Bytes.Vec_String(text))
+  def decode_permissive(text: String): String = {
+    val relevant = {
+      var i = 0
+      val n = text.length
+      var found = false
+      while (i < n && !found) {
+        if (text(i) >= 128) { found = true }
+        i += 1
+      }
+      found
+    }
+    if (relevant) decode_permissive_bytes(new Bytes.Vec_String(text))
     else text
+  }
 }