author | wenzelm |
Sun, 30 May 2010 14:14:30 +0200 | |
changeset 37192 | 8cdddd689ea9 |
parent 29323 | 868634981a32 |
child 60982 | 67e389f67073 |
permissions | -rw-r--r-- |
6316 | 1 |
(* Title: Pure/General/buffer.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
26502 | 4 |
Efficient text buffers. |
6316 | 5 |
*) |
6 |
||
7 |
signature BUFFER = |
|
8 |
sig |
|
9 |
type T |
|
10 |
val empty: T |
|
11 |
val add: string -> T -> T |
|
23785 | 12 |
val markup: Markup.T -> (T -> T) -> T -> T |
6316 | 13 |
val content: T -> string |
26545
6e1aef001b3b
output: canonical argument order (as opposed to write);
wenzelm
parents:
26502
diff
changeset
|
14 |
val output: T -> TextIO.outstream -> unit |
6316 | 15 |
end; |
16 |
||
17 |
structure Buffer: BUFFER = |
|
18 |
struct |
|
19 |
||
29323 | 20 |
datatype T = Buffer of string list; |
6316 | 21 |
|
29323 | 22 |
val empty = Buffer []; |
17062 | 23 |
|
29323 | 24 |
fun add "" buf = buf |
25 |
| add x (Buffer xs) = Buffer (x :: xs); |
|
17062 | 26 |
|
23785 | 27 |
fun markup m body = |
28 |
let val (bg, en) = Markup.output m |
|
29 |
in add bg #> body #> add en end; |
|
30 |
||
29323 | 31 |
fun content (Buffer xs) = implode (rev xs); |
32 |
fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs); |
|
26502 | 33 |
|
6316 | 34 |
end; |