--- 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)
--- 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;