added 'locale' section;
authorwenzelm
Tue Aug 04 18:23:57 1998 +0200 (1998-08-04)
changeset 52486b04b9a88c21
parent 5247 4a8e6e60bbf8
child 5249 9d7e6f7110ef
added 'locale' section;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Aug 04 18:23:28 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Aug 04 18:23:57 1998 +0200
     1.3 @@ -420,6 +420,17 @@
     1.4    >> (fn ((x, y), z) => (cat_lines [x, y, z]));
     1.5  
     1.6  
     1.7 +(* locale *)
     1.8 +
     1.9 +val locale_decl =
    1.10 +  (name --$$ "=") --
    1.11 +    ("fixes" $$--
    1.12 +      (repeat (name --$$ "::" -- !! (typ -- opt_mixfix)) >> (mk_big_list o map mk_triple2))) --
    1.13 +    ("assumes" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair))) --
    1.14 +    ("defines" $$-- (repeat ((ident >> quote) -- !! string) >> (mk_list o map mk_pair)))
    1.15 +  >> (fn (((nm, cs), asms), defs) => cat_lines [nm, cs, asms, defs]);
    1.16 +
    1.17 +
    1.18  
    1.19  (** theory syntax **)
    1.20  
    1.21 @@ -540,7 +551,7 @@
    1.22  val pure_keywords =
    1.23   ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
    1.24    "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>",
    1.25 -  "<="];
    1.26 +  "<=", "fixes", "assumes", "defines"];
    1.27  
    1.28  val pure_sections =
    1.29   [section "classes" "|> Theory.add_classes" class_decls,
    1.30 @@ -561,7 +572,8 @@
    1.31    section "global" "|> PureThy.global_path" empty_decl,
    1.32    section "local" "|> PureThy.local_path" empty_decl,
    1.33    section "setup" "|> Theory.apply" long_id,
    1.34 -  section "MLtext" "" verbatim];
    1.35 +  section "MLtext" "" verbatim,
    1.36 +  section "locale" "|> Locale.add_locale" locale_decl];
    1.37  
    1.38  
    1.39  end;