minor performance tuning;
authorwenzelm
Sat, 15 Jun 2024 20:49:15 +0200
changeset 80374 4f1374f56c0b
parent 80373 dc220d47b85e
child 80375 c33d017fc1a6
minor performance tuning;
src/Pure/General/bytes.scala
--- 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)
     }
   }