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() } } }