# HG changeset patch
# User wenzelm
# Date 1718114553 -7200
# Node ID 7a6cba7c77c9572ba1d0e2a59dc6a1c60fcb9692
# Parent  dbbe26afc31960dfe7a467434596283e8f8a1f69
minor performance tuning;

diff -r dbbe26afc319 -r 7a6cba7c77c9 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jun 11 15:49:39 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jun 11 16:02:33 2024 +0200
@@ -173,7 +173,12 @@
     a
   }
 
-  def text: String = UTF8.decode_permissive_bytes(this)
+  def text: String =
+    if (is_empty) ""
+    else if (iterator.forall((b: Byte) => b >= 0)) {
+      new String(bytes, offset, length, UTF8.charset)
+    }
+    else UTF8.decode_permissive_bytes(this)
 
   def wellformed_text: Option[String] = {
     val s = text
diff -r dbbe26afc319 -r 7a6cba7c77c9 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Tue Jun 11 15:49:39 2024 +0200
+++ b/src/Pure/General/utf8.scala	Tue Jun 11 16:02:33 2024 +0200
@@ -51,17 +51,18 @@
       }
     }
     for (i <- 0L until size) {
-      val b = bytes(i)
-      if (b < 128) { flush(); buf.append(b.toChar) }
-      else if ((b & 0xC0) == 0x80) push(b & 0x3F)
-      else if ((b & 0xE0) == 0xC0) init(b & 0x1F, 1)
-      else if ((b & 0xF0) == 0xE0) init(b & 0x0F, 2)
-      else if ((b & 0xF8) == 0xF0) init(b & 0x07, 3)
+      val c = bytes(i)
+      if (c < 128) { flush(); buf.append(c.toChar) }
+      else if ((c & 0xC0) == 0x80) push(c & 0x3F)
+      else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
+      else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
+      else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
     }
     flush()
     buf.toString
   }
 
   def decode_permissive(text: String): String =
-    decode_permissive_bytes(new Bytes.Vec_String(text))
+    if (text.forall((c: Char) => c < 128)) text
+    else decode_permissive_bytes(new Bytes.Vec_String(text))
 }