16 use "thy_syn.ML"; |
16 use "thy_syn.ML"; |
17 use "thm_database.ML"; |
17 use "thm_database.ML"; |
18 use "thy_read.ML"; |
18 use "thy_read.ML"; |
19 |
19 |
20 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
20 structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); |
21 structure ThmDB = ThmdbFUN(val ignore = ["Trueprop", "all", "==>", "=="]); |
21 structure ThmDB = ThmDBFun(); |
22 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB); |
22 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB); |
23 open ThmDB Readthy; |
23 open ThmDB Readthy; |
24 |
24 |
25 (* hide functors; saves space in PolyML *) |
25 (* hide functors; saves space in PolyML *) |
26 functor ThyScanFun() = struct end; |
26 functor ThyScanFun() = struct end; |
27 functor ThyParseFun() = struct end; |
27 functor ThyParseFun() = struct end; |
28 |
28 |
29 fun init_thy_reader () = |
29 fun init_thy_reader () = |
30 use_string |
30 use_string |
31 ["structure ThmDB = \ |
31 ["structure ThmDB = ThmDBFun();", |
32 \ThmdbFUN(val ignore = [\"Trueprop\",\"all\",\"==>\",\"==\"]);", |
|
33 "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ |
32 "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ |
34 \and ThmDB = ThmDB);", |
33 \and ThmDB = ThmDB);", |
35 "Readthy.loaded_thys := !loaded_thys;", |
34 "Readthy.loaded_thys := !loaded_thys;", |
36 "ThmDB.thm_db := !thm_db;", |
35 "ThmDB.thm_db := !thm_db;", |
37 "val first_init_readthy = false;", |
36 "val first_init_readthy = false;", |