src/Pure/General/buffer.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 29323 868634981a32
child 60982 67e389f67073
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/buffer.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Efficient text buffers.
     5 *)
     6 
     7 signature BUFFER =
     8 sig
     9   type T
    10   val empty: T
    11   val add: string -> T -> T
    12   val markup: Markup.T -> (T -> T) -> T -> T
    13   val content: T -> string
    14   val output: T -> TextIO.outstream -> unit
    15 end;
    16 
    17 structure Buffer: BUFFER =
    18 struct
    19 
    20 datatype T = Buffer of string list;
    21 
    22 val empty = Buffer [];
    23 
    24 fun add "" buf = buf
    25   | add x (Buffer xs) = Buffer (x :: xs);
    26 
    27 fun markup m body =
    28   let val (bg, en) = Markup.output m
    29   in add bg #> body #> add en end;
    30 
    31 fun content (Buffer xs) = implode (rev xs);
    32 fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs);
    33 
    34 end;