--- a/src/Pure/General/bytes.scala Sat Jun 15 20:44:09 2024 +0200
+++ b/src/Pure/General/bytes.scala Sat Jun 15 20:49:15 2024 +0200
@@ -156,6 +156,7 @@
}
final class Builder private[Bytes](chunks_size: Int, buffer_size: Int) {
+ private var size = 0L
private var chunks = new ArrayBuffer[Array[Byte]](chunks_size)
private var buffer = new ByteArrayOutputStream(buffer_size)
@@ -173,6 +174,7 @@
else {
synchronized {
for (i <- 0 until n) {
+ size += 1
buffer.write(s.charAt(i).toByte)
buffer_check()
}
@@ -194,6 +196,7 @@
if (m > 0) {
val l = m min n
buffer.write(array, i, l)
+ size += l
i += l
n -= l
}
@@ -212,7 +215,7 @@
val b = buffer.toByteArray
chunks = null
buffer = null
- new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, make_size(cs, b))
+ new Bytes(if (cs.isEmpty) None else Some(cs), b, 0L, size)
}
}