diff -r d637611b41bd -r b3c65c984210 src/Pure/General/buffer.ML
--- 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;