simple string buffers;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/buffer.ML	Tue Mar 09 12:08:50 1999 +0100
@@ -0,0 +1,27 @@
+(*  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;