# HG changeset patch
# User berghofe
# Date 870819314 -7200
# Node ID 5366dde08dbaf44578ac71b08e97b160efb9e9e1
# Parent  89cbba12863d55ee2a0c457d80df955b5a4a8020
Added some additional "use" commands for new files
(browser_info.ML and thy_info.ML)

diff -r 89cbba12863d -r 5366dde08dba 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 *)