--- a/src/Pure/Thy/ROOT.ML Thu May 19 16:26:19 1994 +0200
+++ b/src/Pure/Thy/ROOT.ML Thu May 19 16:27:16 1994 +0200
@@ -1,36 +1,42 @@
-(* 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"]
-
- val symbols = [",", "<", "{", "}", "(", ")", "(*", "*)",
- "[", "]", "::", "=", "+", "==", "=>", "<="]
- end;
+(* FIXME tmp hack *)
-structure Lex = LexicalFUN (Keyword);
-structure Parse = ParseFUN (Lex);
-structure ThySyn = ThySynFUN (Parse);
+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;
-(*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";
+