back to more elementary Buffer.T -- less intermediate garbage;

--- a/src/Pure/General/buffer.ML	Sat Nov 02 13:25:58 2019 +0100
+++ b/src/Pure/General/buffer.ML	Sat Nov 02 13:37:15 2019 +0100
@@ -9,48 +9,28 @@
   type T
   val empty: T
   val is_empty: T -> bool
-  val chunks: T -> string list
   val content: T -> string
   val add: string -> T -> T
+  val output: T -> (string -> unit) -> unit
   val markup: Markup.T -> (T -> T) -> T -> T
-  val output: T -> BinIO.outstream -> unit
 end;
 
 structure Buffer: BUFFER =
 struct
 
-abstype T = Buffer of {chunk_size: int, chunk: string list, buffer: string list}
+abstype T = Buffer of string list
 with
 
-val empty = Buffer {chunk_size = 0, chunk = [], buffer = []};
-
-fun is_empty (Buffer {chunk, buffer, ...}) = null chunk andalso null buffer;
-
-local
-  val chunk_limit = 4096;
+val empty = Buffer [];
 
-  fun add_chunk [] buffer = buffer
-    | add_chunk chunk buffer = implode (rev chunk) :: buffer;
-in
-
-fun chunks (Buffer {chunk, buffer, ...}) = rev (add_chunk chunk buffer);
-
-val content = implode o chunks;
+fun is_empty (Buffer xs) = null xs;
 
-fun add x (buf as Buffer {chunk_size, chunk, buffer}) =
-  let val n = size x in
-    if n = 0 then buf
-    else if n + chunk_size < chunk_limit then
-      Buffer {chunk_size = n + chunk_size, chunk = x :: chunk, buffer = buffer}
-    else
-      Buffer {chunk_size = 0, chunk = [],
-        buffer =
-          if n < chunk_limit
-          then add_chunk (x :: chunk) buffer
-          else x :: add_chunk chunk buffer}
-  end;
+fun add "" buf = buf
+  | add x (Buffer xs) = Buffer (x :: xs);
 
-end;
+fun content (Buffer xs) = implode (rev xs);
+
+fun output (Buffer xs) out = List.app out (rev xs);
 
 end;
 
@@ -58,7 +38,4 @@
   let val (bg, en) = Markup.output m
   in add bg #> body #> add en end;
 
-fun output buf stream =
-  List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
-
 end;

--- a/src/Pure/General/file.ML	Sat Nov 02 13:25:58 2019 +0100
+++ b/src/Pure/General/file.ML	Sat Nov 02 13:37:15 2019 +0100
@@ -165,7 +165,7 @@
 fun append path txt = append_list path [txt];
 fun generate path txt = if try read path = SOME txt then () else write path txt;
 
-fun write_buffer path buf = open_output (Buffer.output buf) path;
+fun write_buffer path buf = open_output (Buffer.output buf o output) path;
 
 
 (* eq *)