author | wenzelm |
Sun, 20 May 2018 15:05:45 +0200 | |
changeset 68228 | 326f4bcc5abc |
parent 60982 | 67e389f67073 |
child 70600 | 6e97e31933a6 |
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 |
68228 | 14 |
val chunks: T -> string list |
60982
67e389f67073
precise BinIO, without newline conversion on Windows;
wenzelm
parents:
29323
diff
changeset
|
15 |
val output: T -> BinIO.outstream -> unit |
6316 | 16 |
end; |
17 |
||
18 |
structure Buffer: BUFFER = |
|
19 |
struct |
|
20 |
||
29323 | 21 |
datatype T = Buffer of string list; |
6316 | 22 |
|
29323 | 23 |
val empty = Buffer []; |
17062 | 24 |
|
29323 | 25 |
fun add "" buf = buf |
26 |
| add x (Buffer xs) = Buffer (x :: xs); |
|
17062 | 27 |
|
23785 | 28 |
fun markup m body = |
29 |
let val (bg, en) = Markup.output m |
|
30 |
in add bg #> body #> add en end; |
|
31 |
||
29323 | 32 |
fun content (Buffer xs) = implode (rev xs); |
60982
67e389f67073
precise BinIO, without newline conversion on Windows;
wenzelm
parents:
29323
diff
changeset
|
33 |
|
68228 | 34 |
|
35 |
(* chunks *) |
|
36 |
||
37 |
local |
|
38 |
||
39 |
val max_chunk = 4096; |
|
40 |
||
41 |
fun add_chunk [] res = res |
|
42 |
| add_chunk chunk res = implode chunk :: res; |
|
43 |
||
44 |
fun rev_chunks [] _ chunk res = add_chunk chunk res |
|
45 |
| rev_chunks (x :: xs) len chunk res = |
|
46 |
let |
|
47 |
val n = size x; |
|
48 |
val len' = len + n; |
|
49 |
in |
|
50 |
if len' < max_chunk then rev_chunks xs len' (x :: chunk) res |
|
51 |
else rev_chunks xs n [x] (add_chunk chunk res) |
|
52 |
end; |
|
53 |
||
54 |
in |
|
55 |
||
56 |
fun chunks (Buffer xs) = rev_chunks xs 0 [] []; |
|
57 |
||
58 |
fun output buf stream = |
|
59 |
List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf); |
|
26502 | 60 |
|
6316 | 61 |
end; |
68228 | 62 |
|
63 |
end; |