# HG changeset patch
# User wenzelm
# Date 1718488024 -7200
# Node ID 94d903234f6b3e8509effaa2a8e20bed0ba99990
# Parent  1f1ce661c71c7c0558030bcbda91abcd226e0f08
Bytes.Builder is unsynchronized, like java.io.OutputBuffer;

diff -r 1f1ce661c71c -r 94d903234f6b src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 23:24:24 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 23:47:04 2024 +0200
@@ -140,7 +140,7 @@
   }
 
 
-  /* incremental builder: synchronized */
+  /* incremental builder: unsynchronized! */
 
   private def make_size(chunks: Array[Array[Byte]], buffer: Array[Byte]): Long =
     chunks.foldLeft(buffer.length.toLong)((n, chunk) => n + chunk.length)
@@ -177,7 +177,7 @@
         buffer = new ByteArrayOutputStream
       }
 
-    def += (b: Byte): Unit = synchronized {
+    def += (b: Byte): Unit = {
       size += 1
       buffer.write(b)
       buffer_check()
@@ -188,12 +188,10 @@
       if (n > 0) {
         if (UTF8.relevant(s)) { this += UTF8.bytes(s.toString) }
         else {
-          synchronized {
-            for (i <- 0 until n) {
-              size += 1
-              buffer.write(s.charAt(i).toByte)
-              buffer_check()
-            }
+          for (i <- 0 until n) {
+            size += 1
+            buffer.write(s.charAt(i).toByte)
+            buffer_check()
           }
         }
       }
@@ -204,20 +202,18 @@
         throw new IndexOutOfBoundsException
       }
       else if (length > 0) {
-        synchronized {
-          var i = offset
-          var n = length
-          while (n > 0) {
-            val m = buffer_free()
-            if (m > 0) {
-              val l = m min n
-              buffer.write(array, i, l)
-              size += l
-              i += l
-              n -= l
-            }
-            buffer_check()
+        var i = offset
+        var n = length
+        while (n > 0) {
+          val m = buffer_free()
+          if (m > 0) {
+            val l = m min n
+            buffer.write(array, i, l)
+            size += l
+            i += l
+            n -= l
           }
+          buffer_check()
         }
       }
     }
@@ -226,7 +222,7 @@
 
     def += (a: Subarray): Unit = { this += (a.array, a.offset, a.length) }
 
-    private[Bytes] def done(): Bytes = synchronized {
+    private[Bytes] def done(): Bytes = {
       val cs = chunks.toArray
       val b = buffer.toByteArray
       chunks = null