diff -r 4f1374f56c0b -r c33d017fc1a6 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Jun 15 20:49:15 2024 +0200 +++ b/src/Pure/General/bytes.scala Sat Jun 15 21:07:23 2024 +0200 @@ -147,18 +147,18 @@ object Builder { def use(hint: Long = 0L)(body: Builder => Unit): Bytes = { - val chunks_size = if (hint <= 0) 16 else (hint / chunk_size).toInt - val buffer_size = if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt - val builder = new Builder(chunks_size, buffer_size) + val builder = new Builder(hint) body(builder) builder.done() } } - final class Builder private[Bytes](chunks_size: Int, buffer_size: Int) { + final class Builder private[Bytes](hint: Long) { private var size = 0L - private var chunks = new ArrayBuffer[Array[Byte]](chunks_size) - private var buffer = new ByteArrayOutputStream(buffer_size) + private var chunks = + new ArrayBuffer[Array[Byte]](if (hint <= 0) 16 else (hint / chunk_size).toInt) + private var buffer = + new ByteArrayOutputStream(if (hint <= 0) 1024 else (hint min chunk_size min array_size).toInt) private def buffer_free(): Int = chunk_size.toInt - buffer.size() private def buffer_check(): Unit =