author | wenzelm |
Mon, 30 May 2022 10:52:00 +0200 | |
changeset 75489 | f08fd5048df3 |
parent 74231 | b3c65c984210 |
child 75566 | 389b193af8ae |
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 |
74231 | 12 |
val add: string -> T -> T |
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
|
13 |
val content: T -> string |
74231 | 14 |
val build: (T -> T) -> T |
15 |
val build_content: (T -> T) -> string |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
16 |
val output: T -> (string -> unit) -> unit |
23785 | 17 |
val markup: Markup.T -> (T -> T) -> T -> T |
6316 | 18 |
end; |
19 |
||
20 |
structure Buffer: BUFFER = |
|
21 |
struct |
|
22 |
||
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
23 |
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
|
24 |
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
|
25 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
26 |
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
|
27 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
28 |
fun is_empty (Buffer xs) = null xs; |
6316 | 29 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
30 |
fun add "" buf = buf |
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
31 |
| add x (Buffer xs) = Buffer (x :: xs); |
17062 | 32 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
33 |
fun content (Buffer xs) = implode (rev xs); |
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
34 |
|
74231 | 35 |
fun build (f: T -> T) = f empty; |
36 |
fun build_content f = build f |> content; |
|
37 |
||
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
38 |
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
|
39 |
|
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
|
40 |
end; |
17062 | 41 |
|
23785 | 42 |
fun markup m body = |
43 |
let val (bg, en) = Markup.output m |
|
44 |
in add bg #> body #> add en end; |
|
45 |
||
6316 | 46 |
end; |