equal
deleted
inserted
replaced
|
1 (* Title: Pure/General/buffer.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 |
|
5 Simple string buffers. |
|
6 *) |
|
7 |
|
8 signature BUFFER = |
|
9 sig |
|
10 type T |
|
11 val empty: T |
|
12 val add: string -> T -> T |
|
13 val content: T -> string |
|
14 val write: Path.T -> T -> unit |
|
15 end; |
|
16 |
|
17 structure Buffer: BUFFER = |
|
18 struct |
|
19 |
|
20 datatype T = Buffer of string list; |
|
21 |
|
22 val empty = Buffer []; |
|
23 fun add x (Buffer xs) = Buffer (x :: xs); |
|
24 fun content (Buffer xs) = implode (rev xs); |
|
25 fun write path buffer = File.write path (content buffer); |
|
26 |
|
27 end; |