# HG changeset patch # User nipkow # Date 799076295 -7200 # Node ID e57beb974dd77d7a384aedfdb51c8ec98447876b # Parent c2df11ae8b551c78bf1b0c033613a5181061d487 Added functor f() = struct end to hide functors to save space. diff -r c2df11ae8b55 -r e57beb974dd7 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Apr 28 11:52:43 1995 +0200 +++ b/src/Pure/ROOT.ML Fri Apr 28 15:38:15 1995 +0200 @@ -67,6 +67,23 @@ structure Pure = struct val thy = pure_thy end; structure CPure = struct val thy = cpure_thy end; +(* hide functors; saves space in PolyML *) +functor SymtabFun() = struct end; +functor TypeFun() = struct end; +functor SignFun() = struct end; +functor SequenceFun() = struct end; +functor EnvirFun() = struct end; +functor PatternFun() = struct end; +functor UnifyFun() = struct end; +functor NetFun() = struct end; +functor LogicFun() = struct end; +functor ThmFun() = struct end; +functor DruleFun() = struct end; +functor TacticalFun() = struct end; +functor TacticFun() = struct end; +functor GoalsFun() = struct end; +functor AxClassFun() = struct end; + (*Theory parser and loader*) cd "Thy"; use "ROOT.ML"; diff -r c2df11ae8b55 -r e57beb974dd7 src/Pure/Syntax/ROOT.ML --- a/src/Pure/Syntax/ROOT.ML Fri Apr 28 11:52:43 1995 +0200 +++ b/src/Pure/Syntax/ROOT.ML Fri Apr 28 15:38:15 1995 +0200 @@ -41,3 +41,14 @@ 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; diff -r c2df11ae8b55 -r e57beb974dd7 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Fri Apr 28 11:52:43 1995 +0200 +++ b/src/Pure/Thy/ROOT.ML Fri Apr 28 15:38:15 1995 +0200 @@ -13,6 +13,10 @@ structure ThyParse = ThyParseFun(structure Symtab = Symtab and ThyScan = ThyScan); +(* hide functors; saves space in PolyML *) +functor ThyScanFun() = struct end; +functor ThyParseFun() = struct end; + use "thy_syn.ML"; use "thy_read.ML"; @@ -20,6 +24,8 @@ structure Readthy = ReadthyFUN(structure ThySyn = ThySyn); open Readthy; +(* Do not hide ThySynFun and ReadthyFUN; they are still used *) + fun init_thy_reader () = use_string ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",