# HG changeset patch
# User wenzelm
# Date 1718477049 -7200
# Node ID dc220d47b85ec8627229f82ab2891482def84572
# Parent  6e74f0fc8a526617fbdc187d0324577caa0f59ed
minor performance tuning;
clarified signature;

diff -r 6e74f0fc8a52 -r dc220d47b85e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 20:30:31 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 20:44:09 2024 +0200
@@ -41,11 +41,9 @@
 
   val empty: Bytes = reuse_array(new Array(0))
 
-  def apply(s: CharSequence): Bytes = {
-    val str = s.toString
-    if (str.isEmpty) empty
-    else Builder.use(hint = str.length) { builder => builder += str }
-  }
+  def apply(s: CharSequence): Bytes =
+    if (s.isEmpty) empty
+    else Builder.use(hint = s.length) { builder => builder += s }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
@@ -168,18 +166,20 @@
         buffer = new ByteArrayOutputStream
       }
 
-    def += (string: String): Unit =
-      if (string.nonEmpty) {
-        if (UTF8.relevant(string)) { this += UTF8.bytes(string) }
+    def += (s: CharSequence): Unit = {
+      val n = s.length
+      if (n > 0) {
+        if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) }
         else {
           synchronized {
-            for (c <- string) {
-              buffer.write(c.toByte)
+            for (i <- 0 until n) {
+              buffer.write(s.charAt(i).toByte)
               buffer_check()
             }
           }
         }
       }
+    }
 
     def += (array: Array[Byte], offset: Int, length: Int): Unit = {
       if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {
diff -r 6e74f0fc8a52 -r dc220d47b85e src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Sat Jun 15 20:30:31 2024 +0200
+++ b/src/Pure/General/utf8.scala	Sat Jun 15 20:44:09 2024 +0200
@@ -17,8 +17,8 @@
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
-  def relevant(text: String): Boolean =
-    text.exists((c: Char) => c >= 128)
+  def relevant(c: Char): Boolean = c >= 128
+  def relevant(s: CharSequence): Boolean = (0 until s.length).exists(i => relevant(s.charAt(i)))
 
 
   /* permissive UTF-8 decoding */