delete_tmpfiles (from thy_read.ML);
get_lexicon;
load_thy;

--- a/src/Pure/Thy/thy_syn.ML	Wed Feb 03 17:25:12 1999 +0100
+++ b/src/Pure/Thy/thy_syn.ML	Wed Feb 03 17:26:27 1999 +0100
@@ -2,20 +2,28 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Syntax for thy files.
+Provide syntax for old-style theory files.
 *)
 
+signature BASIC_THY_SYN =
+sig
+  val delete_tmpfiles: bool ref
+end;
+
 signature THY_SYN =
 sig
+  include BASIC_THY_SYN
   val add_syntax: string list ->
     (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
     -> unit
-  val parse: string -> string -> string
+  val get_lexicon: unit -> Scan.lexicon;
+  val load_thy: string -> string list -> unit
 end;
 
 structure ThySyn: THY_SYN =
 struct
 
+
 (* current syntax *)
 
 val keywords = ref ThyParse.pure_keywords;
@@ -26,6 +34,8 @@
 
 val syntax = ref (make_syntax ());
 
+fun get_lexicon () = ThyParse.get_lexicon (! syntax);
+
 
 (* augment syntax *)
 
@@ -35,9 +45,23 @@
   syntax := make_syntax ());
 
 
-(* parse *)
+(* load_thy *)
+
+val delete_tmpfiles = ref true;
 
-fun parse name txt =
-  ThyParse.parse_thy (! syntax) name txt;
+fun load_thy name chs =
+  let
+    val tmp_path = File.tmp_path (ThyLoad.ml_path (name ^ "_thy"));
+    val txt_out = ThyParse.parse_thy (! syntax) chs;
+  in
+    File.write tmp_path txt_out;
+    Use.use_path tmp_path;
+    if ! delete_tmpfiles then File.rm tmp_path else ()
+  end;
+
 
 end;
+
+
+structure BasicThySyn: BASIC_THY_SYN = ThySyn;
+open BasicThySyn;