# HG changeset patch
# User wenzelm
# Date 1720179409 -7200
# Node ID 11ca26978dd4ea5b3bcc270a1b8f7a2b7e807d39
# Parent  bbeb2f2049aa46663ac9b8d966cc6ad9b1505de4
tuned;

diff -r bbeb2f2049aa -r 11ca26978dd4 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Jul 05 13:04:39 2024 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jul 05 13:36:49 2024 +0200
@@ -29,9 +29,6 @@
   private val block_size: Int = 16384  // see java.io.InputStream.DEFAULT_BUFFER_SIZE
   private val chunk_size: Long = Space.MiB(100).bytes
 
-  private def make_size(chunks: Array[Array[Byte]], buffer: Array[Byte]): Long =
-    chunks.foldLeft(buffer.length.toLong)((n, chunk) => n + chunk.length)
-
   class Too_Large(size: Long, limit: Long) extends IndexOutOfBoundsException {
     override def getMessage: String =
       "Bytes too large for particular operation: " +
@@ -302,7 +299,9 @@
     offset != 0L || {
       chunks match {
         case None => size != chunk0.length
-        case Some(cs) => size != Bytes.make_size(cs, chunk0)
+        case Some(cs) =>
+          val physical_size = cs.foldLeft(chunk0.length.toLong)((n, c) => n + c.length)
+          size != physical_size
       }
     }