author | haftmann |
Tue, 23 Sep 2008 18:11:44 +0200 | |
changeset 28337 | 93964076e7b8 |
parent 28027 | 051d5ccbafc5 |
child 29323 | 868634981a32 |
permissions | -rw-r--r-- |
6316 | 1 |
(* Title: Pure/General/buffer.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
26502 | 5 |
Efficient text buffers. |
6316 | 6 |
*) |
7 |
||
8 |
signature BUFFER = |
|
9 |
sig |
|
10 |
type T |
|
11 |
val empty: T |
|
12 |
val add: string -> T -> T |
|
26502 | 13 |
val add_substring: substring -> T -> T |
23785 | 14 |
val markup: Markup.T -> (T -> T) -> T -> T |
6316 | 15 |
val content: T -> string |
26545
6e1aef001b3b
output: canonical argument order (as opposed to write);
wenzelm
parents:
26502
diff
changeset
|
16 |
val output: T -> TextIO.outstream -> unit |
6316 | 17 |
end; |
18 |
||
19 |
structure Buffer: BUFFER = |
|
20 |
struct |
|
21 |
||
26502 | 22 |
(* datatype *) |
23 |
||
24 |
datatype T = |
|
25 |
EmptyBuffer |
|
26 |
| String of string * T |
|
27 |
| Substring of substring * T; |
|
6316 | 28 |
|
26502 | 29 |
val empty = EmptyBuffer; |
30 |
||
17062 | 31 |
|
26502 | 32 |
(* add content *) |
33 |
||
34 |
fun add s buf = if s = "" then buf else String (s, buf); |
|
35 |
fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf); |
|
17062 | 36 |
|
23785 | 37 |
fun markup m body = |
38 |
let val (bg, en) = Markup.output m |
|
39 |
in add bg #> body #> add en end; |
|
40 |
||
26502 | 41 |
|
42 |
(* cumulative content *) |
|
43 |
||
44 |
fun rev_content EmptyBuffer acc = acc |
|
45 |
| rev_content (String (s, buf)) acc = rev_content buf (s :: acc) |
|
46 |
| rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc); |
|
47 |
||
48 |
fun content buf = implode (rev_content buf []); |
|
49 |
||
50 |
||
51 |
(* file output *) |
|
17062 | 52 |
|
26502 | 53 |
fun rev_buffer EmptyBuffer acc = acc |
54 |
| rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc)) |
|
55 |
| rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc)); |
|
6316 | 56 |
|
26545
6e1aef001b3b
output: canonical argument order (as opposed to write);
wenzelm
parents:
26502
diff
changeset
|
57 |
fun output buffer stream = |
26502 | 58 |
let |
59 |
fun rev_output EmptyBuffer = () |
|
60 |
| rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf) |
|
61 |
| rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf); |
|
62 |
in rev_output (rev_buffer buffer empty) end; |
|
63 |
||
6316 | 64 |
end; |