Added
authornipkow
Fri Apr 28 15:38:15 1995 +0200 (1995-04-28)
changeset 1078e57beb974dd7
parent 1077 c2df11ae8b55
child 1079 2f9f2ea26f8f
Added

functor f() = struct end

to hide functors to save space.
src/Pure/ROOT.ML
src/Pure/Syntax/ROOT.ML
src/Pure/Thy/ROOT.ML
     1.1 --- a/src/Pure/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
     1.3 @@ -67,6 +67,23 @@
     1.4  structure Pure = struct val thy = pure_thy end;
     1.5  structure CPure = struct val thy = cpure_thy end;
     1.6  
     1.7 +(* hide functors; saves space in PolyML *)
     1.8 +functor SymtabFun() = struct end;
     1.9 +functor TypeFun() = struct end;
    1.10 +functor SignFun() = struct end;
    1.11 +functor SequenceFun() = struct end;
    1.12 +functor EnvirFun() = struct end;
    1.13 +functor PatternFun() = struct end;
    1.14 +functor UnifyFun() = struct end;
    1.15 +functor NetFun() = struct end;
    1.16 +functor LogicFun() = struct end;
    1.17 +functor ThmFun() = struct end;
    1.18 +functor DruleFun() = struct end;
    1.19 +functor TacticalFun() = struct end;
    1.20 +functor TacticFun() = struct end;
    1.21 +functor GoalsFun() = struct end;
    1.22 +functor AxClassFun() = struct end;
    1.23 +
    1.24  (*Theory parser and loader*)
    1.25  cd "Thy";
    1.26  use "ROOT.ML";
     2.1 --- a/src/Pure/Syntax/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
     2.2 +++ b/src/Pure/Syntax/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
     2.3 @@ -41,3 +41,14 @@
     2.4  structure Syntax = PrivateSyntax.Syntax;
     2.5  structure BasicSyntax = PrivateSyntax.BasicSyntax;
     2.6  
     2.7 +(* hide functors; saves space in PolyML *)
     2.8 +functor PrettyFun() = struct end;
     2.9 +functor LexiconFun() = struct end;
    2.10 +functor AstFun() = struct end;
    2.11 +functor SynExtFun() = struct end;
    2.12 +functor ParserFun() = struct end;
    2.13 +functor TypeExtFun() = struct end;
    2.14 +functor SynTransFun() = struct end;
    2.15 +functor MixfixFun() = struct end;
    2.16 +functor PrinterFun() = struct end;
    2.17 +functor SyntaxFun() = struct end;
     3.1 --- a/src/Pure/Thy/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
     3.2 +++ b/src/Pure/Thy/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
     3.3 @@ -13,6 +13,10 @@
     3.4  structure ThyParse = ThyParseFun(structure Symtab = Symtab
     3.5    and ThyScan = ThyScan);
     3.6  
     3.7 +(* hide functors; saves space in PolyML *)
     3.8 +functor ThyScanFun() = struct end;
     3.9 +functor ThyParseFun() = struct end;
    3.10 +
    3.11  use "thy_syn.ML";
    3.12  use "thy_read.ML";
    3.13  
    3.14 @@ -20,6 +24,8 @@
    3.15  structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
    3.16  open Readthy;
    3.17  
    3.18 +(* Do not hide ThySynFun and ReadthyFUN; they are still used *)
    3.19 +
    3.20  fun init_thy_reader () =
    3.21    use_string
    3.22     ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",