--- a/src/Pure/General/bytes.ML Tue Jun 21 15:40:18 2022 +0200
+++ b/src/Pure/General/bytes.ML Tue Jun 21 15:48:59 2022 +0200
@@ -19,6 +19,7 @@
val empty: T
val add_substring: substring -> T -> T
val add: string -> T -> T
+ val append: T -> T -> T
val build: (T -> T) -> T
val string: string -> T
val buffer: Buffer.T -> T
@@ -70,6 +71,11 @@
end;
+fun append bytes1 bytes2 = (*left-associative*)
+ if is_empty bytes1 then bytes2
+ else if is_empty bytes2 then bytes1
+ else bytes1 |> fold add (contents bytes2);
+
fun build (f: T -> T) = f empty;
val string = build o add;