src/Pure/Thy/ROOT.ML
author nipkow
Fri Apr 28 15:38:15 1995 +0200 (1995-04-28)
changeset 1078 e57beb974dd7
parent 431 da3d07d4349b
child 1132 dfb29abcf3c2
permissions -rw-r--r--
Added

functor f() = struct end

to hide functors to save space.
wenzelm@390
     1
(*  Title:      Pure/Thy/ROOT.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@390
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and
wenzelm@390
     4
                Markus Wenzel and Carsten Clasohm, TU Muenchen
clasohm@0
     5
wenzelm@390
     6
This file builds the theory parser and autoloading system.
clasohm@0
     7
*)
clasohm@0
     8
wenzelm@390
     9
use "thy_scan.ML";
wenzelm@390
    10
use "thy_parse.ML";
wenzelm@390
    11
wenzelm@390
    12
structure ThyScan = ThyScanFun(Scanner);
wenzelm@390
    13
structure ThyParse = ThyParseFun(structure Symtab = Symtab
wenzelm@390
    14
  and ThyScan = ThyScan);
clasohm@0
    15
nipkow@1078
    16
(* hide functors; saves space in PolyML *)
nipkow@1078
    17
functor ThyScanFun() = struct end;
nipkow@1078
    18
functor ThyParseFun() = struct end;
nipkow@1078
    19
wenzelm@413
    20
use "thy_syn.ML";
wenzelm@413
    21
use "thy_read.ML";
clasohm@0
    22
wenzelm@413
    23
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
wenzelm@413
    24
structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
wenzelm@413
    25
open Readthy;
clasohm@0
    26
nipkow@1078
    27
(* Do not hide ThySynFun and ReadthyFUN; they are still used *)
nipkow@1078
    28
wenzelm@413
    29
fun init_thy_reader () =
wenzelm@413
    30
  use_string
wenzelm@413
    31
   ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",
wenzelm@413
    32
    "Readthy.loaded_thys := ! loaded_thys;",
wenzelm@413
    33
    "open Readthy;"];
clasohm@74
    34