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
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";
wenzelm@413
    19
use "thy_read.ML";
clasohm@0
    20
wenzelm@413
    21
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
clasohm@1242
    22
structure ThmDB = ThmDBFUN();
clasohm@1242
    23
structure Simplifier = SimplifierFUN();
clasohm@1242
    24
structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB
clasohm@1242
    25
                               and Simplifier = Simplifier);
clasohm@1141
    26
open ThmDB Readthy;
clasohm@0
    27
clasohm@1132
    28
(* hide functors; saves space in PolyML *)
clasohm@1132
    29
functor ThyScanFun() = struct end;
clasohm@1132
    30
functor ThyParseFun() = struct end;
nipkow@1078
    31
wenzelm@413
    32
fun init_thy_reader () =
wenzelm@413
    33
  use_string
clasohm@1242
    34
   ["structure ThmDB = ThmDBFUN();",
clasohm@1242
    35
    "structure Simplifier = SimplifierFUN();",
clasohm@1132
    36
    "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
clasohm@1242
    37
                                   \and ThmDB = ThmDB \
clasohm@1242
    38
                                   \and Simplifier = Simplifier);",
clasohm@1141
    39
    "Readthy.loaded_thys := !loaded_thys;",
clasohm@1141
    40
    "ThmDB.thm_db := !thm_db;",
clasohm@1141
    41
    "val first_init_readthy = false;",
clasohm@1132
    42
    "open Readthy ThmDB;"];