Added some additional "use" commands for new files
authorberghofe
Wed, 06 Aug 1997 00:15:14 +0200
changeset 3600 5366dde08dba
parent 3599 89cbba12863d
child 3601 43c7912aac8d
Added some additional "use" commands for new files (browser_info.ML and thy_info.ML)
src/Pure/Thy/ROOT.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 *)