# HG changeset patch
# User wenzelm
# Date 1656012356 -7200
# Node ID fc8d64a578e467d8a200c1ad56dd249e5196487d
# Parent  7a0d4c126f79fa9b5619ab13e32085271fc60ed3
more operations;

diff -r 7a0d4c126f79 -r fc8d64a578e4 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Thu Jun 23 21:25:23 2022 +0200
+++ b/src/Pure/General/bytes.ML	Thu Jun 23 21:25:56 2022 +0200
@@ -12,6 +12,7 @@
 sig
   val chunk_size: int
   type T
+  val eq: T * T -> bool
   val length: T -> int
   val contents: T -> string list
   val contents_blob: T -> XML.body
@@ -27,6 +28,7 @@
   val last_string: T -> string option
   val trim_line: T -> T
   val append: T -> T -> T
+  val appends: T list -> T
   val string: string -> T
   val newline: T
   val buffer: Buffer.T -> T
@@ -56,6 +58,10 @@
 
 val compact = implode o rev;
 
+fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) =
+  m = m' andalso n = n' andalso chunks = chunks' andalso
+  (buffer = buffer' orelse compact buffer = compact buffer);
+
 fun contents (Bytes {buffer, chunks, ...}) =
   rev (chunks |> not (null buffer) ? cons (compact buffer));
 
@@ -136,6 +142,8 @@
   else if is_empty bytes2 then bytes1
   else bytes1 |> fold add (contents bytes2);
 
+val appends = build o fold (fn b => fn a => append a b);
+
 val string = build o add;
 
 val newline = string "\n";