tuned;
authorwenzelm
Sat, 15 Jun 2024 21:07:23 +0200
changeset 80375 c33d017fc1a6
parent 80374 4f1374f56c0b
child 80376 201af0b45e57
tuned;
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 =