author | wenzelm |
Wed, 16 Apr 1997 18:17:38 +0200 | |
changeset 2960 | a6b56d03ed0d |
parent 2691 | d696d7e17046 |
child 4696 | ff89fc67cc7a |
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 |
||
18 | 8 |
use "pretty.ML"; |
239 | 9 |
use "lexicon.ML"; |
2361 | 10 |
structure Scanner: SCANNER = Lexicon; |
11 |
use "symbol_font.ML"; |
|
2691 | 12 |
use "token_trans.ML"; |
0 | 13 |
use "ast.ML"; |
239 | 14 |
use "syn_ext.ML"; |
18 | 15 |
use "parser.ML"; |
0 | 16 |
use "type_ext.ML"; |
549
5d904be18774
replaced SExtension by SynTrans (mixfix stuff in Mixfix);
wenzelm
parents:
417
diff
changeset
|
17 |
use "syn_trans.ML"; |
392 | 18 |
use "mixfix.ML"; |
0 | 19 |
use "printer.ML"; |
20 |
use "syntax.ML"; |
|
21 |
||
2361 | 22 |
(*hiding: only the most basic features are opened*) |
1506 | 23 |
structure BasicSyntax: BASIC_SYNTAX = Syntax; |
24 |
open BasicSyntax; |