# HG changeset patch
# User wenzelm
# Date 1718134346 -7200
# Node ID fe123d033e76e2c6c3a9de0be17220a74e03ce65
# Parent  8365f1e7955e1b73c5fe172f7e6f533f9fb62456
clarified signature: pro-forma support for Bytes with size: Long;

diff -r 8365f1e7955e -r fe123d033e76 src/Pure/General/bytes.scala
--- 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)
   }
 }
diff -r 8365f1e7955e -r fe123d033e76 src/Pure/General/http.scala
--- 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)
     }
   }
diff -r 8365f1e7955e -r fe123d033e76 src/Pure/General/sql.scala
--- 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)
     }
diff -r 8365f1e7955e -r fe123d033e76 src/Pure/ML/ml_heap.scala
--- 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
diff -r 8365f1e7955e -r fe123d033e76 src/Pure/PIDE/byte_message.scala
--- 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))
diff -r 8365f1e7955e -r fe123d033e76 src/Pure/PIDE/prover.scala
--- 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)
         }
diff -r 8365f1e7955e -r fe123d033e76 src/Tools/VSCode/src/channel.scala
--- 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] = {
diff -r 8365f1e7955e -r fe123d033e76 src/Tools/jEdit/src/isabelle_export.scala
--- 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 {