--- a/src/Pure/General/bytes.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/General/bytes.scala Tue Jun 11 21:32:26 2024 +0200
@@ -130,7 +130,7 @@
final class Bytes private(
protected val bytes: Array[Byte],
protected val offset: Int,
- val length: Int) extends Bytes.Vec {
+ protected val length: Int) extends Bytes.Vec {
/* equality */
override def equals(that: Any): Boolean = {
@@ -196,9 +196,6 @@
case None => (true, encode_base64)
}
- override def toString: String =
- if (is_empty) "Bytes.empty" else "Bytes(" + Space.bytes(length).print + ")"
-
def proper: Option[Bytes] = if (is_empty) None else Some(this)
def proper_text: Option[String] = if (is_empty) None else Some(text)
@@ -215,6 +212,9 @@
/* Vec operations */
+ override def toString: String =
+ if (is_empty) "Bytes.empty" else "Bytes(" + Space.bytes(size).print + ")"
+
def size: Long = length.toLong
def apply(i: Long): Char =
@@ -248,7 +248,7 @@
/* XZ / Zstd data compression */
def detect_xz: Boolean =
- length >= 6 &&
+ size >= 6 &&
bytes(offset) == 0xFD.toByte &&
bytes(offset + 1) == 0x37.toByte &&
bytes(offset + 2) == 0x7A.toByte &&
@@ -257,7 +257,7 @@
bytes(offset + 5) == 0x00.toByte
def detect_zstd: Boolean =
- length >= 4 &&
+ size >= 4 &&
bytes(offset) == 0x28.toByte &&
bytes(offset + 1) == 0xB5.toByte &&
bytes(offset + 2) == 0x2F.toByte &&
@@ -302,6 +302,6 @@
cache: Compress.Cache = Compress.Cache.none
) : (Boolean, Bytes) = {
val compressed = compress(options = options, cache = cache)
- if (compressed.length < length) (true, compressed) else (false, this)
+ if (compressed.size < size) (true, compressed) else (false, this)
}
}
--- a/src/Pure/General/http.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/General/http.scala Tue Jun 11 21:32:26 2024 +0200
@@ -227,7 +227,7 @@
val encoded_digest = Base64.encode(HexFormat.of().parseHex(SHA1.digest(output).toString))
http.getResponseHeaders.set("Content-Digest", "sha=:" + encoded_digest + ":")
}
- http.sendResponseHeaders(code, if (is_head) -1 else output.length.toLong)
+ http.sendResponseHeaders(code, if (is_head) -1 else output.size)
if (!is_head) using(http.getResponseBody)(output.write_stream)
}
}
--- a/src/Pure/General/sql.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/General/sql.scala Tue Jun 11 21:32:26 2024 +0200
@@ -329,7 +329,8 @@
object bytes {
def update(i: Int, bytes: Bytes): Unit = {
if (bytes == null) rep.setBytes(i, null)
- else rep.setBinaryStream(i, bytes.stream(), bytes.length)
+ else if (bytes.size > Int.MaxValue) throw new IllegalArgumentException
+ else rep.setBinaryStream(i, bytes.stream(), bytes.size.toInt)
}
def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull)
}
--- a/src/Pure/ML/ml_heap.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/ML/ml_heap.scala Tue Jun 11 21:32:26 2024 +0200
@@ -16,7 +16,7 @@
def read_file_digest(heap: Path): Option[SHA1.Digest] = {
if (heap.is_file) {
val bs = Bytes.read_file(heap, offset = File.size(heap) - sha1_length)
- if (bs.length == sha1_length) {
+ if (bs.size == sha1_length) {
val s = bs.text
if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(sha1_prefix.length)))
else None
--- a/src/Pure/PIDE/byte_message.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala Tue Jun 11 21:32:26 2024 +0200
@@ -32,8 +32,8 @@
def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) = {
val msg = read(stream, n)
- val len = msg.length
- (if (len == n) Some(msg) else None, len)
+ val len = msg.size
+ (if (len == n) Some(msg) else None, len.toInt)
}
def read_line(stream: InputStream): Option[Bytes] = {
@@ -53,11 +53,11 @@
/* messages with multiple chunks (arbitrary content) */
- private def make_header(ns: List[Int]): List[Bytes] =
+ private def make_header(ns: List[Long]): List[Bytes] =
List(Bytes(ns.mkString(",")), Bytes.newline)
def write_message(stream: OutputStream, chunks: List[Bytes]): Unit = {
- write(stream, make_header(chunks.map(_.length)) ::: chunks)
+ write(stream, make_header(chunks.map(_.size)) ::: chunks)
flush(stream)
}
@@ -93,7 +93,7 @@
if (is_length(msg) || is_terminated(msg))
error ("Bad content for line message:\n" ++ msg.text.take(100))
- val n = msg.length
+ val n = msg.size
write(stream,
(if (n > 100 || msg.iterator.contains(10)) make_header(List(n + 1)) else Nil) :::
List(msg, Bytes.newline))
--- a/src/Pure/PIDE/prover.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Pure/PIDE/prover.scala Tue Jun 11 21:32:26 2024 +0200
@@ -194,7 +194,7 @@
{
case chunks =>
try {
- Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
+ Bytes(chunks.map(_.size).mkString("", ",", "\n")).write_stream(stream)
chunks.foreach(_.write_stream(stream))
stream.flush
true
@@ -288,7 +288,7 @@
command_input match {
case Some(thread) if thread.is_active() =>
if (trace) {
- val payload = args.foldLeft(0) { case (n, b) => n + b.length }
+ val payload = args.foldLeft(0L) { case (n, b) => n + b.size }
Output.writeln(
"protocol_command " + name + ", args = " + args.length + ", payload = " + payload)
}
--- a/src/Tools/VSCode/src/channel.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Tools/VSCode/src/channel.scala Tue Jun 11 21:32:26 2024 +0200
@@ -39,8 +39,8 @@
private def read_content(n: Int): String = {
val bytes = Bytes.read_stream(in, limit = n)
- if (bytes.length == n) bytes.text
- else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)")
+ if (bytes.size == n) bytes.text
+ else error("Bad message content (unexpected EOF after " + bytes.size + " of " + n + " bytes)")
}
def read(): Option[JSON.T] = {
--- a/src/Tools/jEdit/src/isabelle_export.scala Tue Jun 11 16:48:20 2024 +0200
+++ b/src/Tools/jEdit/src/isabelle_export.scala Tue Jun 11 21:32:26 2024 +0200
@@ -56,7 +56,7 @@
} yield {
val is_dir = entry.name_elems.length > depth
val path = Export.implode_name(theory :: entry.name_elems.take(depth))
- val file_size = if (is_dir) None else Some(entry.bytes.length.toLong)
+ val file_size = if (is_dir) None else Some(entry.bytes.size)
(path, file_size)
}).toSet.toList
(for ((path, file_size) <- entries.iterator) yield {