# HG changeset patch # User wenzelm # Date 769358524 -7200 # Node ID 674d878719bdf48a73afc192b6eb5487303c847f # Parent e960fe156cd8ea15afac99d2dc3cdb6de0fe3d1b *** empty log message *** diff -r e960fe156cd8 -r 674d878719bd src/Pure/Syntax/ROOT.ML --- a/src/Pure/Syntax/ROOT.ML Thu May 19 16:30:56 1994 +0200 +++ b/src/Pure/Syntax/ROOT.ML Thu May 19 16:42:04 1994 +0200 @@ -10,9 +10,10 @@ use "ast.ML"; use "syn_ext.ML"; use "parser.ML"; -(*use "earley0A.ML";*) +(*use "earley0A.ML";*) (* FIXME remove *) use "type_ext.ML"; use "sextension.ML"; +use "mixfix.ML"; use "printer.ML"; use "syntax.ML"; @@ -24,11 +25,16 @@ structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon and SynExt = SynExt); (*structure Earley = EarleyFun(structure Symtab = Symtab and Lexicon = Lexicon - and SynExt = SynExt);*) + and SynExt = SynExt);*) (* FIXME remove *) structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt); -structure SExtension = SExtensionFun(Parser); +structure SExtension = SExtensionFun(structure TypeExt = TypeExt and Parser = Parser); +structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and + SExtension = SExtension); structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt and SExtension = SExtension); structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt - and SExtension = SExtension and Printer = Printer); + and SExtension = SExtension and Mixfix = Mixfix and Printer = Printer); structure BasicSyntax: BASIC_SYNTAX = Syntax; + +structure OldMixfix: SEXTENSION0 = SExtension; (* FIXME *) +