# HG changeset patch
# User wenzelm
# Date 1718475463 -7200
# Node ID 119baa9f8cd033f0cf855e5bac2354717d98d50b
# Parent  8c8a2c483fc78345bce6ae793a74fdb2177a8f7d
tuned;

diff -r 8c8a2c483fc7 -r 119baa9f8cd0 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Jun 15 20:14:53 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 20:17:43 2024 +0200
@@ -160,7 +160,13 @@
   final class Builder private[Bytes](chunks_size: Int, buffer_size: Int) {
     private var chunks = new ArrayBuffer[Array[Byte]](chunks_size)
     private var buffer = new ByteArrayOutputStream(buffer_size)
+
     private def buffer_free(): Int = chunk_size.toInt - buffer.size()
+    private def buffer_check(): Unit =
+      if (buffer_free() == 0) {
+        chunks += buffer.toByteArray
+        buffer = new ByteArrayOutputStream
+      }
 
     def += (array: Array[Byte], offset: Int, length: Int): Unit = {
       if (offset < 0 || length < 0 || offset.toLong + length.toLong > array.length) {
@@ -178,10 +184,7 @@
               i += l
               n -= l
             }
-            if (buffer_free() == 0) {
-              chunks += buffer.toByteArray
-              buffer = new ByteArrayOutputStream
-            }
+            buffer_check()
           }
         }
       }