| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 70998 | 7926d2fc3c4c |
| child 74231 | b3c65c984210 |
| permissions | -rw-r--r-- |
| 6316 | 1 |
(* Title: Pure/General/buffer.ML |
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
2 |
Author: Makarius |
| 6316 | 3 |
|
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
4 |
Scalable text buffers. |
| 6316 | 5 |
*) |
6 |
||
7 |
signature BUFFER = |
|
8 |
sig |
|
9 |
type T |
|
10 |
val empty: T |
|
|
70601
79831e40e2be
more scalable: avoid huge intermediate XML elems;
wenzelm
parents:
70600
diff
changeset
|
11 |
val is_empty: T -> bool |
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
12 |
val content: T -> string |
| 6316 | 13 |
val add: string -> T -> T |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
14 |
val output: T -> (string -> unit) -> unit |
| 23785 | 15 |
val markup: Markup.T -> (T -> T) -> T -> T |
| 6316 | 16 |
end; |
17 |
||
18 |
structure Buffer: BUFFER = |
|
19 |
struct |
|
20 |
||
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
21 |
abstype T = Buffer of string list |
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
22 |
with |
|
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
23 |
|
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
24 |
val empty = Buffer []; |
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
25 |
|
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
26 |
fun is_empty (Buffer xs) = null xs; |
| 6316 | 27 |
|
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
28 |
fun add "" buf = buf |
|
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
29 |
| add x (Buffer xs) = Buffer (x :: xs); |
| 17062 | 30 |
|
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
31 |
fun content (Buffer xs) = implode (rev xs); |
|
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
32 |
|
|
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
33 |
fun output (Buffer xs) out = List.app out (rev xs); |
|
70600
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
34 |
|
|
6e97e31933a6
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents:
68228
diff
changeset
|
35 |
end; |
| 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 |
||
| 6316 | 41 |
end; |