src/Pure/General/buffer.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23785 ea7c2ee8a47a
child 26502 7f64d8cf6707
permissions -rw-r--r--
tuned signature;
wenzelm@6316
     1
(*  Title:      Pure/General/buffer.ML
wenzelm@6316
     2
    ID:         $Id$
wenzelm@6316
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6316
     4
wenzelm@18132
     5
Efficient string buffers.
wenzelm@6316
     6
*)
wenzelm@6316
     7
wenzelm@6316
     8
signature BUFFER =
wenzelm@6316
     9
sig
wenzelm@6316
    10
  type T
wenzelm@6316
    11
  val empty: T
wenzelm@6316
    12
  val add: string -> T -> T
wenzelm@23785
    13
  val markup: Markup.T -> (T -> T) -> T -> T
wenzelm@6316
    14
  val content: T -> string
wenzelm@6316
    15
  val write: Path.T -> T -> unit
aspinall@21630
    16
  val output: (string -> unit) -> T -> unit
wenzelm@6316
    17
end;
wenzelm@6316
    18
wenzelm@6316
    19
structure Buffer: BUFFER =
wenzelm@6316
    20
struct
wenzelm@6316
    21
wenzelm@6316
    22
datatype T = Buffer of string list;
wenzelm@6316
    23
wenzelm@6316
    24
val empty = Buffer [];
wenzelm@17062
    25
wenzelm@17062
    26
fun add "" buf = buf
wenzelm@17062
    27
  | add x (Buffer xs) = Buffer (x :: xs);
wenzelm@17062
    28
wenzelm@23785
    29
fun markup m body =
wenzelm@23785
    30
  let val (bg, en) = Markup.output m
wenzelm@23785
    31
  in add bg #> body #> add en end;
wenzelm@23785
    32
wenzelm@6316
    33
fun content (Buffer xs) = implode (rev xs);
wenzelm@17062
    34
wenzelm@16712
    35
fun write path (Buffer xs) = File.write_list path (rev xs);
wenzelm@6316
    36
wenzelm@23226
    37
fun output f (Buffer xs) = List.app f (rev xs);
aspinall@21630
    38
wenzelm@6316
    39
end;