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