# HG changeset patch
# User wenzelm
# Date 920977730 -3600
# Node ID 4a786a8a1a974386b0d5b910936a2b54a86ba88f
# Parent  ed71bedf6976030648a11a704cc91cd7c6a0292d
simple string buffers;

diff -r ed71bedf6976 -r 4a786a8a1a97 src/Pure/General/buffer.ML
--- /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;