| author | wenzelm | 
| Fri, 31 Jul 1998 11:33:53 +0200 | |
| changeset 5230 | fdc28193ccf7 | 
| parent 4940 | dd4bbbcd1d22 | 
| child 5683 | e62518aacc5b | 
| permissions | -rw-r--r-- | 
| 18 | 1  | 
(* Title: Pure/Syntax/ROOT.ML  | 
| 0 | 2  | 
ID: $Id$  | 
3  | 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen  | 
|
4  | 
||
| 18 | 5  | 
This file builds the syntax module.  | 
| 0 | 6  | 
*)  | 
7  | 
||
| 4940 | 8  | 
(*generic modules*)  | 
| 4696 | 9  | 
use "scan.ML";  | 
| 4940 | 10  | 
use "source.ML";  | 
| 4696 | 11  | 
use "symbol.ML";  | 
| 5230 | 12  | 
use "pretty.ML";  | 
| 4940 | 13  | 
|
14  | 
(*actual syntax module*)  | 
|
| 239 | 15  | 
use "lexicon.ML";  | 
| 2691 | 16  | 
use "token_trans.ML";  | 
| 0 | 17  | 
use "ast.ML";  | 
| 239 | 18  | 
use "syn_ext.ML";  | 
| 18 | 19  | 
use "parser.ML";  | 
| 0 | 20  | 
use "type_ext.ML";  | 
| 
549
 
5d904be18774
replaced SExtension by SynTrans (mixfix stuff in Mixfix);
 
wenzelm 
parents: 
417 
diff
changeset
 | 
21  | 
use "syn_trans.ML";  | 
| 392 | 22  | 
use "mixfix.ML";  | 
| 0 | 23  | 
use "printer.ML";  | 
24  | 
use "syntax.ML";  | 
|
25  | 
||
| 2361 | 26  | 
(*hiding: only the most basic features are opened*)  | 
| 1506 | 27  | 
structure BasicSyntax: BASIC_SYNTAX = Syntax;  | 
28  | 
open BasicSyntax;  |