author | wenzelm |
Thu, 15 Jun 2023 14:28:17 +0200 | |
changeset 78158 | 8b5a2e4b16d4 |
parent 75566 | 389b193af8ae |
child 80822 | 4f54a509bc89 |
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 |
75566 | 13 |
val length: T -> int |
14 |
val contents: T -> 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
|
15 |
val content: T -> string |
74231 | 16 |
val build: (T -> T) -> T |
17 |
val build_content: (T -> T) -> string |
|
23785 | 18 |
val markup: Markup.T -> (T -> T) -> T -> T |
6316 | 19 |
end; |
20 |
||
21 |
structure Buffer: BUFFER = |
|
22 |
struct |
|
23 |
||
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
27 |
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
|
28 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
29 |
fun is_empty (Buffer xs) = null xs; |
6316 | 30 |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
31 |
fun add "" buf = buf |
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
32 |
| add x (Buffer xs) = Buffer (x :: xs); |
17062 | 33 |
|
75566 | 34 |
fun length (Buffer xs) = fold (Integer.add o size) xs 0; |
35 |
||
36 |
fun contents (Buffer xs) = rev xs; |
|
37 |
val content = implode o contents; |
|
70998
7926d2fc3c4c
back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents:
70601
diff
changeset
|
38 |
|
74231 | 39 |
fun build (f: T -> T) = f empty; |
40 |
fun build_content f = build f |> content; |
|
41 |
||
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
|
42 |
end; |
17062 | 43 |
|
23785 | 44 |
fun markup m body = |
45 |
let val (bg, en) = Markup.output m |
|
46 |
in add bg #> body #> add en end; |
|
47 |
||
6316 | 48 |
end; |