--- 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;
-