src/Pure/Thy/ROOT.ML
author clasohm
Wed Oct 04 12:57:50 1995 +0100 (1995-10-04)
changeset 1261 af4107a03150
parent 1242 b3f68a644380
child 1291 e173be970d27
permissions -rw-r--r--
changed usage of structure Simplifier
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
wenzelm@413
    16
use "thy_syn.ML";
clasohm@1132
    17
use "thm_database.ML";
clasohm@1242
    18
use "../../Provers/simplifier.ML";
clasohm@1261
    19
clasohm@1261
    20
structure Simplifier = SimplifierFun();
clasohm@1261
    21
wenzelm@413
    22
use "thy_read.ML";
clasohm@0
    23
wenzelm@413
    24
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
clasohm@1261
    25
structure ThmDB = ThmDBFun();
clasohm@1261
    26
structure Readthy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
clasohm@1141
    27
open ThmDB Readthy;
clasohm@0
    28
clasohm@1132
    29
(* hide functors; saves space in PolyML *)
clasohm@1132
    30
functor ThyScanFun() = struct end;
clasohm@1132
    31
functor ThyParseFun() = struct end;
clasohm@1261
    32
functor SimplifierFun() = struct end;
nipkow@1078
    33
wenzelm@413
    34
fun init_thy_reader () =
wenzelm@413
    35
  use_string
clasohm@1261
    36
   ["structure ThmDB = ThmDBFun();",
clasohm@1261
    37
    "structure Readthy = ReadthyFun(structure ThySyn = ThySyn \
clasohm@1261
    38
                                   \and ThmDB = ThmDB);",
clasohm@1141
    39
    "Readthy.loaded_thys := !loaded_thys;",
clasohm@1141
    40
    "ThmDB.thm_db := !thm_db;",
clasohm@1261
    41
    "open ThmDB Readthy;"];