tuned;
authorwenzelm
Sat, 15 Jun 2024 20:17:43 +0200
changeset 80370 119baa9f8cd0
parent 80369 8c8a2c483fc7
child 80371 e43944fae5e5
tuned;
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()
           }
         }
       }