# HG changeset patch # User wenzelm # Date 1566393571 -7200 # Node ID 6e97e31933a697f011fa3cfc5c8c534e84e456a2 # Parent 8539476439711230024de2a7238d74dbd6d5e8a8 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management; diff -r 853947643971 -r 6e97e31933a6 src/Pure/General/buffer.ML --- 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;