Added some additional "use" commands for new files
authorberghofe
Wed Aug 06 00:15:14 1997 +0200 (1997-08-06)
changeset 36005366dde08dba
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
     1.1 --- a/src/Pure/Thy/ROOT.ML	Wed Aug 06 00:06:47 1997 +0200
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Wed Aug 06 00:15:14 1997 +0200
     1.3 @@ -9,32 +9,16 @@
     1.4  use "thy_scan.ML";
     1.5  use "thy_parse.ML";
     1.6  use "thy_syn.ML";
     1.7 +use "thy_info.ML";
     1.8 +use "browser_info.ML";
     1.9  use "thm_database.ML";
    1.10  use "symbol_input.ML";
    1.11  use "thy_read.ML";
    1.12  
    1.13 -structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    1.14 -structure ThmDB = ThmDBFun();
    1.15 -structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
    1.16 -open ThmDB ReadThy SymbolInput;
    1.17 -
    1.18 +open ThmDB ReadThy ThyInfo BrowserInfo SymbolInput;
    1.19  
    1.20 -fun init_thy_reader () =
    1.21 -  use_string
    1.22 -   ["structure ThmDB = ThmDBFun();",
    1.23 -    "structure ReadThy = ReadthyFun(structure ThySyn = ThySyn \
    1.24 -                                   \and ThmDB = ThmDB);",
    1.25 -    "ReadThy.loaded_thys := !loaded_thys;",
    1.26 -    "map ReadThy.set_thy_reader_file (!thy_reader_files);",
    1.27 -    "ReadThy.base_path := !base_path;",
    1.28 -    "ReadThy.gif_path := !gif_path;",
    1.29 -    "ReadThy.index_path := !index_path;",
    1.30 -    "ReadThy.pure_subchart := !pure_subchart;",
    1.31 -    "ReadThy.make_html := !make_html;",
    1.32 -    "ThmDB.thm_db := !thm_db;",
    1.33 -    "open ThmDB ReadThy;",
    1.34 -    "read_thy_reader_files ();"];
    1.35 -
    1.36 +structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    1.37 +set_parser ThySyn.parse;
    1.38  
    1.39  (* FIXME tmp *)
    1.40