src/Pure/Thy/ROOT.ML
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 2404 edcc26b1461d
child 2809 174d03b1798f
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
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@413
    11
use "thy_syn.ML";
clasohm@1132
    12
use "thm_database.ML";
clasohm@1242
    13
use "../../Provers/simplifier.ML";
wenzelm@2404
    14
use "symbol_input.ML";
wenzelm@413
    15
use "thy_read.ML";
clasohm@0
    16
wenzelm@413
    17
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
clasohm@1261
    18
structure ThmDB = ThmDBFun();
clasohm@1291
    19
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
wenzelm@2404
    20
open ThmDB ReadThy SymbolInput;
clasohm@0
    21
nipkow@1078
    22
wenzelm@413
    23
fun init_thy_reader () =
wenzelm@413
    24
  use_string
clasohm@1261
    25
   ["structure ThmDB = ThmDBFun();",
clasohm@1291
    26
    "structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \
clasohm@1261
    27
                                   \and ThmDB = ThmDB);",
clasohm@1291
    28
    "ReadThy.loaded_thys := !loaded_thys;",
clasohm@1457
    29
    "map ReadThy.set_thy_reader_file (!thy_reader_files);",
clasohm@1348
    30
    "ReadThy.base_path := !base_path;",
clasohm@1291
    31
    "ReadThy.gif_path := !gif_path;",
clasohm@1313
    32
    "ReadThy.index_path := !index_path;",
clasohm@1348
    33
    "ReadThy.pure_subchart := !pure_subchart;",
clasohm@1291
    34
    "ReadThy.make_html := !make_html;",
clasohm@1141
    35
    "ThmDB.thm_db := !thm_db;",
clasohm@1457
    36
    "open ThmDB ReadThy;",
clasohm@1457
    37
    "read_thy_reader_files ();"];