eliminated ThySynData and ThySynFun;
added ThySyn.add_syntax;

--- a/src/Pure/Thy/ROOT.ML	Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/ROOT.ML	Wed Aug 06 11:52:16 1997 +0200
@@ -9,16 +9,16 @@
 use "thy_scan.ML";
 use "thy_parse.ML";
 use "thy_syn.ML";
+
 use "thy_info.ML";
 use "browser_info.ML";
 use "thm_database.ML";
+
 use "symbol_input.ML";
 use "thy_read.ML";
 
-open ThmDB ReadThy ThyInfo BrowserInfo SymbolInput;
+open ThmDB ThyRead ThyInfo BrowserInfo SymbolInput;
 
-structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
-set_parser ThySyn.parse;
 
 (* FIXME tmp *)
 

--- a/src/Pure/Thy/thy_read.ML	Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Aug 06 11:52:16 1997 +0200
@@ -7,7 +7,7 @@
 Functions for reading theory files.
 *)
 
-signature READTHY =
+signature THY_READ =
 sig
   datatype basetype = Thy  of string
                     | File of string
@@ -15,8 +15,6 @@
   val loadpath       : string list ref
   val delete_tmpfiles: bool ref
 
-  val set_parser     : (string -> string -> string) -> unit
-
   val use_thy        : string -> unit
   val time_use_thy   : string -> unit
   val use_dir        : string -> unit
@@ -27,7 +25,7 @@
 end;
 
 
-structure ReadThy : READTHY =
+structure ThyRead: THY_READ =
 struct
 
 open ThmDB ThyInfo BrowserInfo;
@@ -37,14 +35,6 @@
                   | File of string;
 
 
-(*parser for theory files*)
-val parser = ref ((K (K "")):string -> string -> string);
-
-
-(*set parser for theory files*)
-fun set_parser p = parser := p;
-
-
 (*Default search path for theory files*)
 val loadpath = ref ["."];
 
@@ -66,12 +56,13 @@
 fun read_thy tname thy_file =
   let
     val instream  = TextIO.openIn thy_file;
+    val intext = TextIO.inputAll instream;
+    val _ = TextIO.closeIn instream;
+    val outext = ThySyn.parse tname intext;
     val outstream = TextIO.openOut (out_name tname);
-  in
-    TextIO.output (outstream, (!parser) tname (TextIO.inputAll instream));
-    TextIO.closeOut outstream;
-    TextIO.closeIn instream
-  end;
+    val _ = TextIO.output (outstream, outext);
+    val _ = TextIO.closeOut outstream;
+  in () end;
 
 
 (*Check if a theory was completly loaded *)

--- a/src/Pure/Thy/thy_syn.ML	Wed Aug 06 11:19:59 1997 +0200
+++ b/src/Pure/Thy/thy_syn.ML	Wed Aug 06 11:52:16 1997 +0200
@@ -2,29 +2,42 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Interface for user syntax.
+Syntax for thy files.
 *)
 
-signature THY_SYN_DATA =
-  sig
-  val user_keywords: string list
-  val user_sections: (string * (ThyParse.token list -> (string * string)
-    * ThyParse.token list)) list
-  end;
-
 signature THY_SYN =
-  sig
+sig
+  val add_syntax: string list ->
+    (string * (ThyParse.token list -> (string * string) * ThyParse.token list)) list
+    -> unit
   val parse: string -> string -> string
-  end;
+end;
 
-functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
+structure ThySyn: THY_SYN =
 struct
 
-val syntax =
-  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
-		       (ThyParse.pure_sections @ Data.user_sections);
+(* current syntax *)
+
+val keywords = ref ThyParse.pure_keywords;
+val sections = ref ThyParse.pure_sections;
+
+fun make_syntax () =
+  ThyParse.make_syntax (! keywords) (!sections);
+
+val syntax = ref (make_syntax ());
+
 
-val parse = ThyParse.parse_thy syntax;
+(* augment syntax *)
+
+fun add_syntax keys sects =
+ (keywords := keys union ! keywords;
+  sections := sects @ ! sections;
+  syntax := make_syntax ());
+
+
+(* parse *)
+
+fun parse name txt =
+  ThyParse.parse_thy (! syntax) name txt;
 
 end;
-