src/Pure/Thy/ROOT.ML
author paulson
Tue, 22 Jul 1997 11:14:18 +0200
changeset 3538 ed9de44032e0
parent 2809 174d03b1798f
child 3576 9cd0a0919ba0
permissions -rw-r--r--
Removal of the tactical STATE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     1
(*  Title:      Pure/Thy/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     3
    Author:     Sonia Mahjoub and Tobias Nipkow and
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     4
                Markus Wenzel and Carsten Clasohm, TU Muenchen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     6
This file builds the theory parser and autoloading system.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
390
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
     9
use "thy_scan.ML";
b074205ac50a *** empty log message ***
wenzelm
parents: 74
diff changeset
    10
use "thy_parse.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    11
use "thy_syn.ML";
1132
dfb29abcf3c2 added theorem database which contains axioms and theorems indexed by the
clasohm
parents: 1078
diff changeset
    12
use "thm_database.ML";
1242
b3f68a644380 added cleanup of global simpset to thy_read;
clasohm
parents: 1221
diff changeset
    13
use "../../Provers/simplifier.ML";
2404
edcc26b1461d added symbol_input.ML;
wenzelm
parents: 1512
diff changeset
    14
use "symbol_input.ML";
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    15
use "thy_read.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    17
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
1261
af4107a03150 changed usage of structure Simplifier
clasohm
parents: 1242
diff changeset
    18
structure ThmDB = ThmDBFun();
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1261
diff changeset
    19
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
2404
edcc26b1461d added symbol_input.ML;
wenzelm
parents: 1512
diff changeset
    20
open ThmDB ReadThy SymbolInput;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
1078
nipkow
parents: 431
diff changeset
    22
413
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    23
fun init_thy_reader () =
2a1554524ad5 removed garbage;
wenzelm
parents: 390
diff changeset
    24
  use_string
1261
af4107a03150 changed usage of structure Simplifier
clasohm
parents: 1242
diff changeset
    25
   ["structure ThmDB = ThmDBFun();",
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1261
diff changeset
    26
    "structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \
1261
af4107a03150 changed usage of structure Simplifier
clasohm
parents: 1242
diff changeset
    27
                                   \and ThmDB = ThmDB);",
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1261
diff changeset
    28
    "ReadThy.loaded_thys := !loaded_thys;",
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1348
diff changeset
    29
    "map ReadThy.set_thy_reader_file (!thy_reader_files);",
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1313
diff changeset
    30
    "ReadThy.base_path := !base_path;",
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1261
diff changeset
    31
    "ReadThy.gif_path := !gif_path;",
1313
9fb65f3db319 renamed chart00 and 00-chart to "index"
clasohm
parents: 1291
diff changeset
    32
    "ReadThy.index_path := !index_path;",
1348
b9305143fa91 index.html files are now made separatly for each subdirectory
clasohm
parents: 1313
diff changeset
    33
    "ReadThy.pure_subchart := !pure_subchart;",
1291
e173be970d27 added generation of HTML files to thy_read.ML;
clasohm
parents: 1261
diff changeset
    34
    "ReadThy.make_html := !make_html;",
1141
a94c0ab9a3ed commented thms_unifying_with out; placed thm_db into signature again;
clasohm
parents: 1135
diff changeset
    35
    "ThmDB.thm_db := !thm_db;",
1457
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1348
diff changeset
    36
    "open ThmDB ReadThy;",
ad856378ad62 added facility to associate arbitrary data with theories
clasohm
parents: 1348
diff changeset
    37
    "read_thy_reader_files ();"];
2809
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    38
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    39
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    40
(* FIXME tmp *)
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    41
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    42
fun set_session s =
174d03b1798f added dummy set_session;
wenzelm
parents: 2404
diff changeset
    43
  writeln ("This is the " ^ quote s ^ " session.");