Added some additional "use" commands for new files
(browser_info.ML and thy_info.ML)
--- a/src/Pure/Thy/ROOT.ML Wed Aug 06 00:06:47 1997 +0200
+++ b/src/Pure/Thy/ROOT.ML Wed Aug 06 00:15:14 1997 +0200
@@ -9,32 +9,16 @@
use "thy_scan.ML";
use "thy_parse.ML";
use "thy_syn.ML";
+use "thy_info.ML";
+use "browser_info.ML";
use "thm_database.ML";
use "symbol_input.ML";
use "thy_read.ML";
-structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
-structure ThmDB = ThmDBFun();
-structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
-open ThmDB ReadThy SymbolInput;
-
+open ThmDB ReadThy ThyInfo BrowserInfo SymbolInput;
-fun init_thy_reader () =
- use_string
- ["structure ThmDB = ThmDBFun();",
- "structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \
- \and ThmDB = ThmDB);",
- "ReadThy.loaded_thys := !loaded_thys;",
- "map ReadThy.set_thy_reader_file (!thy_reader_files);",
- "ReadThy.base_path := !base_path;",
- "ReadThy.gif_path := !gif_path;",
- "ReadThy.index_path := !index_path;",
- "ReadThy.pure_subchart := !pure_subchart;",
- "ReadThy.make_html := !make_html;",
- "ThmDB.thm_db := !thm_db;",
- "open ThmDB ReadThy;",
- "read_thy_reader_files ();"];
-
+structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
+set_parser ThySyn.parse;
(* FIXME tmp *)