author | paulson |
Fri, 18 Feb 2000 15:35:29 +0100 | |
changeset 8255 | 38f96394c099 |
parent 7767 | 659648e14c3e |
child 8806 | a202293db3f6 |
permissions | -rw-r--r-- |
(* Title: Pure/General/buffer.ML ID: $Id$ Author: Markus Wenzel, TU Muenchen Simple 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 x (Buffer xs) = Buffer (x :: xs); fun content (Buffer xs) = implode (rev xs); fun write path buffer = File.write path (content buffer); end;