src/Pure/Thy/ROOT.ML
author clasohm
Fri Sep 01 13:28:54 1995 +0200 (1995-09-01)
changeset 1242 b3f68a644380
parent 1221 19dde7bfcd07
child 1261 af4107a03150
permissions -rw-r--r--
added cleanup of global simpset to thy_read;
replaced error by warning for duplicate names in theorem database
     1 (*  Title:      Pure/Thy/ROOT.ML
     2     ID:         $Id$
     3     Author:     Sonia Mahjoub and Tobias Nipkow and
     4                 Markus Wenzel and Carsten Clasohm, TU Muenchen
     5 
     6 This file builds the theory parser and autoloading system.
     7 *)
     8 
     9 use "thy_scan.ML";
    10 use "thy_parse.ML";
    11 
    12 structure ThyScan = ThyScanFun(Scanner);
    13 structure ThyParse = ThyParseFun(structure Symtab = Symtab
    14   and ThyScan = ThyScan);
    15 
    16 use "thy_syn.ML";
    17 use "thm_database.ML";
    18 use "../../Provers/simplifier.ML";
    19 use "thy_read.ML";
    20 
    21 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    22 structure ThmDB = ThmDBFUN();
    23 structure Simplifier = SimplifierFUN();
    24 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB
    25                                and Simplifier = Simplifier);
    26 open ThmDB Readthy;
    27 
    28 (* hide functors; saves space in PolyML *)
    29 functor ThyScanFun() = struct end;
    30 functor ThyParseFun() = struct end;
    31 
    32 fun init_thy_reader () =
    33   use_string
    34    ["structure ThmDB = ThmDBFUN();",
    35     "structure Simplifier = SimplifierFUN();",
    36     "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
    37                                    \and ThmDB = ThmDB \
    38                                    \and Simplifier = Simplifier);",
    39     "Readthy.loaded_thys := !loaded_thys;",
    40     "ThmDB.thm_db := !thm_db;",
    41     "val first_init_readthy = false;",
    42     "open Readthy ThmDB;"];