# HG changeset patch
# User wenzelm
# Date 1718476190 -7200
# Node ID e43944fae5e52fcbaeff18e273ae4b09fa374207
# Parent  119baa9f8cd033f0cf855e5bac2354717d98d50b
clarified signature;

diff -r 119baa9f8cd0 -r e43944fae5e5 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Sat Jun 15 20:17:43 2024 +0200
+++ b/src/Pure/General/utf8.scala	Sat Jun 15 20:29:50 2024 +0200
@@ -17,6 +17,9 @@
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
+  def relevant(text: String): Boolean =
+    text.exists((c: Char) => c >= 128)
+
 
   /* permissive UTF-8 decoding */
 
@@ -63,6 +66,6 @@
   }
 
   def decode_permissive(text: String): String =
-    if (text.forall((c: Char) => c < 128)) text
-    else decode_permissive_bytes(new Bytes.Vec_String(text))
+    if (relevant(text)) decode_permissive_bytes(new Bytes.Vec_String(text))
+    else text
 }