diff -r 65a2482f772d -r 389b193af8ae src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Mon Jun 20 10:45:25 2022 +0200
+++ b/src/Pure/General/buffer.ML	Mon Jun 20 16:15:07 2022 +0200
@@ -10,10 +10,11 @@
   val empty: T
   val is_empty: T -> bool
   val add: string -> T -> T
+  val length: T -> int
+  val contents: T -> string list
   val content: T -> string
   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,13 +31,14 @@
 fun add "" buf = buf
   | add x (Buffer xs) = Buffer (x :: xs);
 
-fun content (Buffer xs) = implode (rev xs);
+fun length (Buffer xs) = fold (Integer.add o size) xs 0;
+
+fun contents (Buffer xs) = rev xs;
+val content = implode o contents;
 
 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;
 
 fun markup m body =