--- a/src/Pure/General/buffer.ML Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/General/buffer.ML Sat Sep 04 20:01:43 2021 +0200
@@ -9,8 +9,10 @@
type T
val empty: T
val is_empty: T -> bool
+ val add: string -> T -> T
val content: T -> string
- val add: string -> T -> T
+ val build: (T -> T) -> T
+ val build_content: (T -> T) -> string
val output: T -> (string -> unit) -> unit
val markup: Markup.T -> (T -> T) -> T -> T
end;
@@ -30,6 +32,9 @@
fun content (Buffer xs) = implode (rev xs);
+fun build (f: T -> T) = f empty;
+fun build_content f = build f |> content;
+
fun output (Buffer xs) out = List.app out (rev xs);
end;