src/Pure/Isar/outer_parse.ML
changeset 12272 9bc50336dab6
parent 12268 28e60c998eee
child 12876 a70df1e5bf10
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Nov 22 23:44:57 2001 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Nov 22 23:45:23 2001 +0100
     1.3 @@ -71,6 +71,7 @@
     1.4    val spec_opt_name: token list -> ((bstring * string) * Args.src list) * token list
     1.5    val xthm: token list -> (xstring * Args.src list) * token list
     1.6    val xthms1: token list -> (xstring * Args.src list) list * token list
     1.7 +  val locale_expr: token list -> Locale.expr * token list
     1.8    val locale_element: token list -> Args.src Locale.element * token list
     1.9    val method: token list -> Method.text * token list
    1.10  end;
    1.11 @@ -306,24 +307,34 @@
    1.12  
    1.13  (* locale elements *)
    1.14  
    1.15 -(* FIXME
    1.16 +local
    1.17 +
    1.18 +val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
    1.19 +val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "uses";
    1.20 +
    1.21 +fun plus1 scan =
    1.22 +  scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
    1.23 +
    1.24  fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
    1.25  and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
    1.26 -and expr0 x = (enum1 "+" expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.27 -*)
    1.28 -val expr0 = xname;
    1.29 +and expr0 x = (plus1 expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.30  
    1.31 -val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
    1.32 +in
    1.33 +
    1.34 +val locale_expr = expr0;
    1.35  
    1.36  val locale_element = group "locale element"
    1.37    ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
    1.38 -    >> triple1)) >> Locale.Fixes ||
    1.39 +    >> triple1)) >> (Locale.Elem o Locale.Fixes) ||
    1.40    $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
    1.41 -    >> Locale.Assumes ||
    1.42 +    >> (Locale.Elem o Locale.Assumes) ||
    1.43    $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
    1.44 -    >> Locale.Defines ||
    1.45 -  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
    1.46 -  $$$ "uses" |-- !!! expr0 >> (Locale.Uses o Locale.Locale));
    1.47 +    >> (Locale.Elem o Locale.Defines) ||
    1.48 +  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
    1.49 +    >> (Locale.Elem o Locale.Notes) ||
    1.50 +  $$$ "uses" |-- !!! locale_expr >> Locale.Expr);
    1.51 +
    1.52 +end;
    1.53  
    1.54  
    1.55  (* proof methods *)