src/Pure/Syntax/ROOT.ML
changeset 1506 192c48376d25
parent 1078 e57beb974dd7
child 2198 0dddd9575717
--- a/src/Pure/Syntax/ROOT.ML	Fri Feb 16 13:55:29 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Fri Feb 16 14:06:09 1996 +0100
@@ -16,39 +16,8 @@
 use "printer.ML";
 use "syntax.ML";
 
-structure PrivateSyntax =
-struct
-  structure Pretty = PrettyFun();
-  structure Lexicon = LexiconFun();
-  structure Scanner: SCANNER = Lexicon;
-  structure Ast = AstFun(Pretty);
-  structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast);
-  structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
-    and SynExt = SynExt);
-  structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
-  structure SynTrans = SynTransFun(structure TypeExt = TypeExt and Parser = Parser);
-  structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and
-    SynTrans = SynTrans);
-  structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt
-    and SynTrans = SynTrans);
-  structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
-    and SynTrans = SynTrans and Mixfix = Mixfix and Printer = Printer);
-  structure BasicSyntax: BASIC_SYNTAX = Syntax;
-end;
+(*Hiding: only the most basic features are opened*)
+structure BasicSyntax: BASIC_SYNTAX = Syntax;
+open BasicSyntax;
 
-structure Pretty = PrivateSyntax.Pretty;
-structure Scanner = PrivateSyntax.Scanner;
-structure Syntax = PrivateSyntax.Syntax;
-structure BasicSyntax = PrivateSyntax.BasicSyntax;
-
-(* hide functors; saves space in PolyML *)
-functor PrettyFun() = struct end;
-functor LexiconFun() = struct end;
-functor AstFun() = struct end;
-functor SynExtFun() = struct end;
-functor ParserFun() = struct end;
-functor TypeExtFun() = struct end;
-functor SynTransFun() = struct end;
-functor MixfixFun() = struct end;
-functor PrinterFun() = struct end;
-functor SyntaxFun() = struct end;
+structure Scanner: SCANNER = Lexicon;