clarified signature;
authorwenzelm
Fri, 05 Jul 2024 12:53:45 +0200
changeset 80509 2a9abd6a164e
parent 80508 8585399f26f6
child 80510 bbeb2f2049aa
clarified signature;
src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Fri Jul 05 11:38:21 2024 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jul 05 12:53:45 2024 +0200
@@ -32,10 +32,10 @@
   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) extends IndexOutOfBoundsException {
+  class Too_Large(size: Long, limit: Long) extends IndexOutOfBoundsException {
     override def getMessage: String =
       "Bytes too large for particular operation: " +
-        Space.bytes(size).print + " > " + Space.bytes(array_size).print
+        Space.bytes(size).print + " > " + Space.bytes(limit).print
   }
 
 
@@ -294,10 +294,6 @@
       chunks.get.forall(chunk => chunk.length == Bytes.chunk_size)) &&
     chunk0.length < Bytes.chunk_size)
 
-  def small_size: Int =
-    if (size > Bytes.array_size) throw new Bytes.Too_Large(size)
-    else size.toInt
-
   override def is_empty: Boolean = size == 0
 
   def proper: Option[Bytes] = if (is_empty) None else Some(bytes)
@@ -479,7 +475,10 @@
     }
 
   def make_array: Array[Byte] = {
-    val buf = new ByteArrayOutputStream(small_size)
+    val n =
+      if (size <= Bytes.array_size) size.toInt
+      else throw new Bytes.Too_Large(size, Bytes.array_size)
+    val buf = new ByteArrayOutputStream(n)
     for (a <- subarray_iterator) { buf.write(a.array, a.offset, a.length) }
     buf.toByteArray
   }