src/Pure/Thy/ROOT.ML

-(*  Title:      Pure/Thy/ROOT
+(*  Title:      Pure/Thy/ROOT.ML
     ID:         $Id$
-    Author:     Sonia Mahjoub / Tobias Nipkow
-    Copyright   1992  TU Muenchen
+    Author:     Sonia Mahjoub and Tobias Nipkow and
+                Markus Wenzel and Carsten Clasohm, TU Muenchen
 
-This file builds the theory parser.
-It assumes the standard Isabelle environment.
+This file builds the theory parser and autoloading system.
 *)
 
-use "scan.ML";
-use "parse.ML";
-use "syntax.ML";
-use "read.ML";
+(* 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;
 
 
-structure Keyword =
-    struct
-    val alphas =  ["classes", "default", "arities", "types",
-                   "consts", "rules", "end", "rules", "mixfix",
-                   "infixr", "infixl", "binder", "translations"]
+(* FIXME tmp hack *)
 
-    val symbols = [",", "<", "{", "}", "(", ")", "(*", "*)",
-                   "[", "]", "::", "=", "+", "==", "=>", "<="]
-    end;
+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 Lex     = LexicalFUN (Keyword);
-structure Parse   = ParseFUN (Lex);
-structure ThySyn  = ThySynFUN (Parse);
 
-(*This structure is only defined to be compatible with older versions of
-  READTHY. Don't use it in newly created theory/ROOT.ML files! Instead
-  define a new structure. Otherwise Poly/ML won't save a reference variable
-  defined inside the functor. *)
-structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
-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";