# HG changeset patch
# User wenzelm
# Date 926437883 -7200
# Node ID 6f74e7aa5b4d2ca8bba38cf63e10021ff111d461
# Parent  2ed30ebd7e31ee38efccc2384749aad2841fa71f
moved scan.ML;

diff -r 2ed30ebd7e31 -r 6f74e7aa5b4d src/Pure/General/README
--- a/src/Pure/General/README	Tue May 11 10:33:26 1999 +0200
+++ b/src/Pure/General/README	Tue May 11 17:51:23 1999 +0200
@@ -13,11 +13,11 @@
   Seq           (unbounded sequences)
   NameSpace     (hierarchically structured name spaces)
   Position      (input positions)
+  Scan          (generic scanner toolbox)
   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)
   Symbol        (generalized characters)
   Pretty        (generic pretty printing module)
diff -r 2ed30ebd7e31 -r 6f74e7aa5b4d src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Tue May 11 10:33:26 1999 +0200
+++ b/src/Pure/General/ROOT.ML	Tue May 11 17:51:23 1999 +0200
@@ -10,11 +10,11 @@
 use "seq.ML";
 use "name_space.ML";
 use "position.ML";
+use "scan.ML";
 use "path.ML";
 use "file.ML";
 use "buffer.ML";
 use "history.ML";
-use "scan.ML";
 use "source.ML";
 use "symbol.ML";
 use "pretty.ML";
@@ -27,11 +27,11 @@
   structure Seq = Seq;
   structure NameSpace = NameSpace;
   structure Position = Position;
+  structure Scan = Scan;
   structure Path = Path;
   structure File = File;
   structure Buffer = Buffer;
   structure History = History;
-  structure Scan = Scan;
   structure Source = Source;
   structure Symbol = Symbol;
   structure Pretty = Pretty;