# HG changeset patch # User wenzelm # Date 889456023 -3600 # Node ID 49d116fdcafac802f92e4579e78133d5de99f5ce # Parent 033566671199c568024f43179558a7e9a6d6b5aa tuned; diff -r 033566671199 -r 49d116fdcafa src/Pure/README --- 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) diff -r 033566671199 -r 49d116fdcafa src/Pure/Syntax/README --- 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.