equal
deleted
inserted
replaced
18 struct |
18 struct |
19 |
19 |
20 datatype T = Buffer of string list; |
20 datatype T = Buffer of string list; |
21 |
21 |
22 val empty = Buffer []; |
22 val empty = Buffer []; |
23 fun add x (Buffer xs) = Buffer (x :: xs); |
23 |
|
24 fun add "" buf = buf |
|
25 | add x (Buffer xs) = Buffer (x :: xs); |
|
26 |
24 fun content (Buffer xs) = implode (rev xs); |
27 fun content (Buffer xs) = implode (rev xs); |
|
28 |
25 fun write path (Buffer xs) = File.write_list path (rev xs); |
29 fun write path (Buffer xs) = File.write_list path (rev xs); |
26 |
30 |
27 end; |
31 end; |