# HG changeset patch
# User wenzelm
# Date 902247837 -7200
# Node ID 6b04b9a88c21927bb9530252289998fd92bd8de9
# Parent  4a8e6e60bbf89b965b8d5d056bc501ef0f7bfbe9
added 'locale' section;

diff -r 4a8e6e60bbf8 -r 6b04b9a88c21 src/Pure/Thy/thy_parse.ML
--- 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;