# HG changeset patch # User wenzelm # Date 1720179973 -7200 # Node ID 482897a69699573dcf05f06dac6565c938a2bd78 # Parent 4d142545b86b956b42f7912cb144e7c671928dc1 tuned signature: expose internal limits for testing or add-on implementations; diff -r 4d142545b86b -r 482897a69699 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Fri Jul 05 13:41:01 2024 +0200 +++ b/src/Pure/General/bytes.scala Fri Jul 05 13:46:13 2024 +0200 @@ -22,12 +22,12 @@ object Bytes { - /* internal sizes */ + /* internal limits */ - private val array_size: Long = Int.MaxValue - 8 // see java.io.InputStream.MAX_BUFFER_SIZE - private val string_size: Long = Int.MaxValue / 2 - private val block_size: Int = 16384 // see java.io.InputStream.DEFAULT_BUFFER_SIZE - private val chunk_size: Long = Space.MiB(100).bytes + val array_size: Long = Int.MaxValue - 8 // see java.io.InputStream.MAX_BUFFER_SIZE + val string_size: Long = Int.MaxValue / 2 + val block_size: Int = 16384 // see java.io.InputStream.DEFAULT_BUFFER_SIZE + val chunk_size: Long = Space.MiB(100).bytes class Too_Large(size: Long, limit: Long) extends IndexOutOfBoundsException { override def getMessage: String =