author | wenzelm |
Wed, 09 Nov 2005 16:26:47 +0100 | |
changeset 18132 | 0e9c9a18f454 |
parent 17062 | 7272b45099c7 |
child 21630 | d1ca26a2b918 |
permissions | -rw-r--r-- |
(* Title: Pure/General/buffer.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Efficient string buffers. *) signature BUFFER = sig type T val empty: T val add: string -> T -> T val content: T -> string val write: Path.T -> T -> unit end; structure Buffer: BUFFER = struct datatype T = Buffer of string list; val empty = Buffer []; fun add "" buf = buf | add x (Buffer xs) = Buffer (x :: xs); fun content (Buffer xs) = implode (rev xs); fun write path (Buffer xs) = File.write_list path (rev xs); end;