--- a/src/Pure/General/bytes.ML Tue Jun 21 15:56:31 2022 +0200
+++ b/src/Pure/General/bytes.ML Tue Jun 21 16:03:00 2022 +0200
@@ -33,6 +33,8 @@
structure Bytes: BYTES =
struct
+(* primitive operations *)
+
val chunk_size = 1024 * 1024;
abstype T = Bytes of
@@ -71,6 +73,9 @@
end;
+
+(* derived operations *)
+
fun append bytes1 bytes2 = (*left-associative*)
if is_empty bytes1 then bytes2
else if is_empty bytes2 then bytes1
@@ -97,6 +102,9 @@
val read = File.open_input read_stream;
val write = File.open_output write_stream;
+
+(* ML pretty printing *)
+
val _ =
ML_system_pp (fn _ => fn _ => fn bytes =>
PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}"))