# HG changeset patch
# User wenzelm
# Date 1718476231 -7200
# Node ID 6e74f0fc8a526617fbdc187d0324577caa0f59ed
# Parent  e43944fae5e52fcbaeff18e273ae4b09fa374207
minor performance tuning;

diff -r e43944fae5e5 -r 6e74f0fc8a52 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 20:29:50 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 20:30:31 2024 +0200
@@ -168,6 +168,19 @@
         buffer = new ByteArrayOutputStream
       }
 
+    def += (string: String): Unit =
+      if (string.nonEmpty) {
+        if (UTF8.relevant(string)) { this += UTF8.bytes(string) }
+        else {
+          synchronized {
+            for (c <- string) {
+              buffer.write(c.toByte)
+              buffer_check()
+            }
+          }
+        }
+      }
+
     def += (array: Array[Byte], offset: Int, length: Int): Unit = {
       if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {
         throw new IndexOutOfBoundsException
@@ -194,8 +207,6 @@
 
     def += (a: Subarray): Unit = { this += (a.array, a.offset, a.length) }
 
-    def += (string: String): Unit = if (string.nonEmpty) { this += UTF8.bytes(string) }
-
     private def done(): Bytes = synchronized {
       val cs = chunks.toArray
       val b = buffer.toByteArray