--- a/src/Pure/Thy/thy_parse.ML Tue Aug 04 18:23:28 1998 +0200
+++ b/src/Pure/Thy/thy_parse.ML Tue Aug 04 18:23:57 1998 +0200
@@ -420,6 +420,17 @@
>> (fn ((x, y), z) => (cat_lines [x, y, z]));
+(* locale *)
+
+val locale_decl =
+ (name --$$ "=") --
+ ("fixes" $$--
+ (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) >> (mk_big_list o map mk_triple2))) --
+ ("assumes" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair))) --
+ ("defines" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair)))
+ >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]);
+
+
(** theory syntax **)
@@ -540,7 +551,7 @@
val pure_keywords =
["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
"+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>",
- "<="];
+ "<=", "fixes", "assumes", "defines"];
val pure_sections =
[section "classes" "|> Theory.add_classes" class_decls,
@@ -561,7 +572,8 @@
section "global" "|> PureThy.global_path" empty_decl,
section "local" "|> PureThy.local_path" empty_decl,
section "setup" "|> Theory.apply" long_id,
- section "MLtext" "" verbatim];
+ section "MLtext" "" verbatim,
+ section "locale" "|> Locale.add_locale" locale_decl];
end;