added Source module;
authorwenzelm
Mon, 18 May 1998 18:10:04 +0200
changeset 4940 dd4bbbcd1d22
parent 4939 33af5d3dae1f
child 4941 ac5da3e767b0
added Source module;
src/Pure/Syntax/README
src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/README	Mon May 18 18:08:58 1998 +0200
+++ b/src/Pure/Syntax/README	Mon May 18 18:10:04 1998 +0200
@@ -8,7 +8,8 @@
 
   Pretty        (generic pretty printing module)
   Scan          (generic scanner toolbox)
-  Symbol	(baroque characters)
+  Source	(co-algebraic data sources)
+  Symbol	(generalized characters)
 
   Syntax        (internal interface to the syntax module)
   BasicSyntax   (part of Syntax made pervasive)
--- a/src/Pure/Syntax/ROOT.ML	Mon May 18 18:08:58 1998 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Mon May 18 18:10:04 1998 +0200
@@ -5,9 +5,13 @@
 This file builds the syntax module.
 *)
 
+(*generic modules*)
 use "pretty.ML";
 use "scan.ML";
+use "source.ML";
 use "symbol.ML";
+
+(*actual syntax module*)
 use "lexicon.ML";
 use "token_trans.ML";
 use "ast.ML";