# HG changeset patch
# User wenzelm
# Date 770478447 -7200
# Node ID 2a1554524ad5943f2c66cc4011d9ff7fda7c3160
# Parent  216624270b80f45fbb9f4d1884bcd1a0959778ef
removed garbage;
adapted to new ThySyn (interface for 'user sections');

diff -r 216624270b80 -r 2a1554524ad5 src/Pure/Thy/ROOT.ML
--- a/src/Pure/Thy/ROOT.ML	Wed Jun 01 15:46:11 1994 +0200
+++ b/src/Pure/Thy/ROOT.ML	Wed Jun 01 15:47:27 1994 +0200
@@ -9,34 +9,24 @@
 (* FIXME remove (still needed by HOL/Datatype.ML) *)
 use "scan.ML"; use "parse.ML";
 
+
 use "thy_scan.ML";
 use "thy_parse.ML";
-use "thy_read.ML";
 
 structure ThyScan = ThyScanFun(Scanner);
 structure ThyParse = ThyParseFun(structure Symtab = Symtab
   and ThyScan = ThyScan);
-structure ThyRead = ThyReadFun(structure ThyParse = ThyParse);
-open ThyRead;
 
-
-(* FIXME tmp hack *)
+use "thy_syn.ML";
+use "thy_read.ML";
 
-fun eval txt =
-  let
-    val tmp_name = "/tmp/.eval.tmp";
-    val tmp_file = open_out tmp_name;
-  in
-    output (tmp_file, txt);
-    close_out tmp_file;
-    use tmp_name;
-    delete_file tmp_name
-  end;
+structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
+structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
+open Readthy;
 
+fun init_thy_reader () =
+  use_string
+   ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",
+    "Readthy.loaded_thys := ! loaded_thys;",
+    "open Readthy;"];
 
-fun init_thy_reader () = 
-  eval   (* FIXME use_string *)
-    "structure ThyRead = ThyReadFun(structure ThyParse = ThyParse);\n\
-    \ThyRead.loaded_thys := ! loaded_thys;\n\
-    \open ThyRead;\n";
-