# HG changeset patch
# User wenzelm
# Date 920977745 -3600
# Node ID 128e592f54896874b747f5a3360c48441593e9d4
# Parent  4a786a8a1a974386b0d5b910936a2b54a86ba88f
added Buffer;

diff -r 4a786a8a1a97 -r 128e592f5489 src/Pure/General/README
--- a/src/Pure/General/README	Tue Mar 09 12:08:50 1999 +0100
+++ b/src/Pure/General/README	Tue Mar 09 12:09:05 1999 +0100
@@ -15,6 +15,7 @@
   Position      (input positions)
   Path          (abstract algebra of file paths)
   File          (file system operations)
+  Buffer	(simple string buffers)
   History       (histories of values, with undo and redo)
   Scan          (generic scanner toolbox)
   Source        (co-algebraic data sources)
diff -r 4a786a8a1a97 -r 128e592f5489 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Tue Mar 09 12:08:50 1999 +0100
+++ b/src/Pure/General/ROOT.ML	Tue Mar 09 12:09:05 1999 +0100
@@ -12,6 +12,7 @@
 use "position.ML";
 use "path.ML";
 use "file.ML";
+use "buffer.ML";
 use "history.ML";
 use "scan.ML";
 use "source.ML";
@@ -28,6 +29,7 @@
   structure Position = Position;
   structure Path = Path;
   structure File = File;
+  structure Buffer = Buffer;
   structure History = History;
   structure Scan = Scan;
   structure Source = Source;