--- a/src/Pure/README Mon Mar 09 16:06:46 1998 +0100
+++ b/src/Pure/README Mon Mar 09 16:07:03 1998 +0100
@@ -1,12 +1,15 @@
+
Pure: The Pure Isabelle System
+
This directory contains the ML source files for Pure Isabelle, which
is the basis for all object-logics:
- IsaMakefile compiles the Pure system
+ IsaMakefile compiles the Pure system (use isatool make)
ML-Systems/ compatibility files for various ML systems
Syntax/ the syntax module
Thy/ the theory file parser and loader
+ ./ the actual meta logic implementation (see ROOT.ML)
Isabelle programmers may want to have a look at the following generic
modules:
@@ -15,6 +18,8 @@
TableFun efficient tables (see table.ML)
Seq unbounded sequences (see seq.ML)
Pretty pretty printing module (see Syntax/pretty.ML)
- Scanner scanner toolbox (see Syntax/lexicon.ML)
+ Scan scanner toolbox (see Syntax/scan.ML)
+ Symbol baroque characters (see Syntax/symbol.ML)
Path abstract algebra of file paths (see Thy/path.ML)
File file system operations (see Thy/file.ML)
+ NameSpace hierarchically structured name spaces (see name_space.ML)
--- a/src/Pure/Syntax/README Mon Mar 09 16:06:46 1998 +0100
+++ b/src/Pure/Syntax/README Mon Mar 09 16:07:03 1998 +0100
@@ -1,14 +1,14 @@
+
Pure/Syntax/
-This directory contains the source files for Isabelle's syntax module, which
-includes a lexer, parser, pretty printer and macro system. Note that only the
-following structures are supposed to be exported:
+
+This directory contains the source files for Isabelle's syntax module,
+which includes a lexer, parser, pretty printer and macro system. Note
+that only the following structures are supposed to be exported:
Pretty (generic pretty printing module)
- Scanner (generic scanner toolbox)
+ Scan (generic scanner toolbox)
+ Symbol (baroque characters)
Syntax (internal interface to the syntax module)
BasicSyntax (part of Syntax made pervasive)
-
-There is no IsaMakefile to compile these files separately; they are
-compiled as part of Pure Isabelle.