src/Pure/Syntax/ROOT.ML
changeset 163 ad90d96c2ec3
parent 47 0af9dbb93529
child 239 08b6e842ec16
equal deleted inserted replaced
162:58d54dc482d1 163:ad90d96c2ec3
    37 structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
    37 structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
    38   and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
    38   and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
    39 structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
    39 structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
    40   and Parser = Earley and SExtension = SExtension and Printer = Printer);
    40   and Parser = Earley and SExtension = SExtension and Printer = Printer);
    41 
    41 
       
    42 structure Scanner: SCANNER = Lexicon;
    42 
    43 
    43 (*BasicSyntax has the most important primitives, which are made pervasive*)
    44 (*BasicSyntax has the most important primitives, which are made pervasive*)
    44 signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;
    45 signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;
    45 structure BasicSyntax: BASIC_SYNTAX = Syntax;
    46 structure BasicSyntax: BASIC_SYNTAX = Syntax;
    46 
    47