| changeset 23226 | 441f8a0bd766 |
| parent 21630 | d1ca26a2b918 |
| child 23785 | ea7c2ee8a47a |
| 23225:591af6a2f09e | 23226:441f8a0bd766 |
|---|---|
27 |
27 |
28 fun content (Buffer xs) = implode (rev xs); |
28 fun content (Buffer xs) = implode (rev xs); |
29 |
29 |
30 fun write path (Buffer xs) = File.write_list path (rev xs); |
30 fun write path (Buffer xs) = File.write_list path (rev xs); |
31 |
31 |
32 fun output f (Buffer xs) = Library.seq f (rev xs); |
32 fun output f (Buffer xs) = List.app f (rev xs); |
33 |
33 |
34 end; |
34 end; |