# HG changeset patch
# User wenzelm
# Date 1720966651 -7200
# Node ID 2acdaa0a7d297c957b7da539c5091e7d739af942
# Parent  2309ac831dd475e12a55c314f1b818bece10b573
clarified signature, following Isabelle/Scala;

diff -r 2309ac831dd4 -r 2acdaa0a7d29 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Sun Jul 14 16:07:03 2024 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Sun Jul 14 16:17:31 2024 +0200
@@ -51,7 +51,7 @@
   val xml = export_proof thy1 @{thm Int.times_int.abs_eq};
   val thm = import_proof thy1 xml;
 
-  val xml_size = Bytes.length (YXML.bytes_of_body xml);
+  val xml_size = Bytes.size (YXML.bytes_of_body xml);
   \<^assert> (xml_size > 10000000);
 \<close>
 
diff -r 2309ac831dd4 -r 2acdaa0a7d29 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Sun Jul 14 16:07:03 2024 +0200
+++ b/src/Pure/General/bytes.ML	Sun Jul 14 16:17:31 2024 +0200
@@ -13,7 +13,7 @@
   val chunk_size: int
   type T
   val eq: T * T -> bool
-  val length: T -> int
+  val size: T -> int
   val contents: T -> string list
   val contents_blob: T -> XML.body
   val content: T -> string
@@ -54,7 +54,7 @@
   {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}
 with
 
-fun length (Bytes {m, n, ...}) = m + n;
+fun size (Bytes {m, n, ...}) = m + n;
 
 val compact = implode o rev;
 
@@ -69,7 +69,7 @@
 
 val content = implode o contents;
 
-fun is_empty bytes = length bytes = 0;
+fun is_empty bytes = size bytes = 0;
 
 val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0};
 
@@ -132,10 +132,10 @@
 fun beginning n bytes =
   let
     val dots = " ...";
-    val m = (String.maxSize - size dots) div chunk_size;
+    val m = (String.maxSize - String.size dots) div chunk_size;
     val a = implode (take m (contents bytes));
-    val b = String.substring (a, 0, Int.min (n, size a));
-  in if size b < length bytes then b ^ dots else b end;
+    val b = String.substring (a, 0, Int.min (n, String.size a));
+  in if String.size b < size bytes then b ^ dots else b end;
 
 fun append bytes1 bytes2 =  (*left-associative*)
   if is_empty bytes1 then bytes2
@@ -155,7 +155,7 @@
 
 fun space_explode sep bytes =
   if is_empty bytes then []
-  else if size sep <> 1 then [content bytes]
+  else if String.size sep <> 1 then [content bytes]
   else
     let
       val sep_char = String.nth sep 0;
@@ -199,7 +199,7 @@
 fun read_stream limit stream =
   let
     fun read bytes =
-      (case read_block (limit - length bytes) stream of
+      (case read_block (limit - size bytes) stream of
         "" => bytes
       | s => read (add s bytes))
   in read empty end;
@@ -216,6 +216,6 @@
 
 val _ =
   ML_system_pp (fn _ => fn _ => fn bytes =>
-    PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}"))
+    PolyML.PrettyString ("Bytes {size = " ^ string_of_int (size bytes) ^ "}"))
 
 end;
diff -r 2309ac831dd4 -r 2acdaa0a7d29 src/Pure/PIDE/byte_message.ML
--- a/src/Pure/PIDE/byte_message.ML	Sun Jul 14 16:07:03 2024 +0200
+++ b/src/Pure/PIDE/byte_message.ML	Sun Jul 14 16:17:31 2024 +0200
@@ -44,7 +44,7 @@
 fun read_block stream n =
   let
     val msg = read stream n;
-    val len = Bytes.length msg;
+    val len = Bytes.size msg;
   in (if len = n then SOME msg else NONE, len) end;
 
 fun read_line stream =
@@ -66,7 +66,7 @@
   [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline];
 
 fun write_message stream chunks =
-  (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream);
+  (write stream (make_header (map Bytes.size chunks) @ chunks); flush stream);
 
 fun write_message_string stream =
   write_message stream o map Bytes.string;
@@ -110,7 +110,7 @@
   if is_length msg orelse is_terminated msg then
     error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg)
   else
-    let val n = Bytes.length msg in
+    let val n = Bytes.size msg in
       write stream
         ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg
           then make_header [n + 1] else []) @ [msg, Bytes.newline]);