more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;

--- a/src/Pure/General/buffer.ML	Tue Aug 20 22:01:37 2019 +0200
+++ b/src/Pure/General/buffer.ML	Wed Aug 21 15:19:31 2019 +0200
@@ -1,63 +1,61 @@
 (*  Title:      Pure/General/buffer.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Efficient text buffers.
+Scalable text buffers.
 *)
 
 signature BUFFER =
 sig
   type T
   val empty: T
+  val chunks: T -> string list
+  val content: T -> string
   val add: string -> T -> T
   val markup: Markup.T -> (T -> T) -> T -> T
-  val content: T -> string
-  val chunks: T -> string list
   val output: T -> BinIO.outstream -> unit
 end;
 
 structure Buffer: BUFFER =
 struct
 
-datatype T = Buffer of string list;
+abstype T = Buffer of {chunk_size: int, chunk: string list, buffer: string list}
+with
+
+val empty = Buffer {chunk_size = 0, chunk = [], buffer = []};
+
+local
+  val chunk_limit = 4096;
+
+  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;
 
-val empty = Buffer [];
+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;
+
+end;
 
 fun markup m body =
   let val (bg, en) = Markup.output m
   in add bg #> body #> add en end;
 
-fun content (Buffer xs) = implode (rev xs);
-
-
-(* chunks *)
-
-local
-
-val max_chunk = 4096;
-
-fun add_chunk [] res = res
-  | add_chunk chunk res = implode chunk :: res;
-
-fun rev_chunks [] _ chunk res = add_chunk chunk res
-  | rev_chunks (x :: xs) len chunk res =
-      let
-        val n = size x;
-        val len' = len + n;
-      in
-        if len' < max_chunk then rev_chunks xs len' (x :: chunk) res
-        else rev_chunks xs n [x] (add_chunk chunk res)
-      end;
-
-in
-
-fun chunks (Buffer xs) = rev_chunks xs 0 [] [];
-
 fun output buf stream =
   List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
 
 end;
-
-end;