src/Pure/Syntax/ROOT.ML
changeset 4696 ff89fc67cc7a
parent 2691 d696d7e17046
child 4940 dd4bbbcd1d22
equal deleted inserted replaced
4695:6aa25ee18fc4 4696:ff89fc67cc7a
     4 
     4 
     5 This file builds the syntax module.
     5 This file builds the syntax module.
     6 *)
     6 *)
     7 
     7 
     8 use "pretty.ML";
     8 use "pretty.ML";
       
     9 use "scan.ML";
       
    10 use "symbol.ML";
     9 use "lexicon.ML";
    11 use "lexicon.ML";
    10 structure Scanner: SCANNER = Lexicon;
       
    11 use "symbol_font.ML";
       
    12 use "token_trans.ML";
    12 use "token_trans.ML";
    13 use "ast.ML";
    13 use "ast.ML";
    14 use "syn_ext.ML";
    14 use "syn_ext.ML";
    15 use "parser.ML";
    15 use "parser.ML";
    16 use "type_ext.ML";
    16 use "type_ext.ML";