src/Pure/Isar/spec_parse.ML
changeset 24869 bad2b2be1f24
parent 24014 d3873741678d
child 25094 ba43514068fd
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Sat Oct 06 16:50:08 2007 +0200
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Sat Oct 06 16:50:09 2007 +0200
     1.3 @@ -23,11 +23,9 @@
     1.4      ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
     1.5    val locale_mixfix: token list -> mixfix * token list
     1.6    val locale_fixes: token list -> (string * string option * mixfix) list * token list
     1.7 -  val locale_insts: token list ->
     1.8 -    (string option list * string list) * token list
     1.9 +  val locale_insts: token list -> (string option list * string list) * token list
    1.10 +  val class_expr: token list -> string list * token list
    1.11    val locale_expr: token list -> Locale.expr * token list
    1.12 -  val locale_expr_unless: (token list -> 'a * token list) ->
    1.13 -    token list -> Locale.expr * token list
    1.14    val locale_keyword: token list -> string * token list
    1.15    val locale_element: token list -> Element.context Locale.element * token list
    1.16    val context_element: token list -> Element.context * token list
    1.17 @@ -108,21 +106,22 @@
    1.18    P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
    1.19      >> (curry Element.Notes "");
    1.20  
    1.21 -fun plus1 test scan =
    1.22 +fun plus1_unless test scan =
    1.23    scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
    1.24  
    1.25  val rename = P.name -- Scan.option P.mixfix;
    1.26  
    1.27 -fun expr test =
    1.28 +in
    1.29 +
    1.30 +val class_expr = plus1_unless loc_keyword P.xname;
    1.31 +
    1.32 +val locale_expr =
    1.33    let
    1.34      fun expr2 x = (P.xname >> Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
    1.35      and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Locale.Rename || expr2) x
    1.36 -    and expr0 x = (plus1 test expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.37 +    and expr0 x = (plus1_unless loc_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.38    in expr0 end;
    1.39 -in
    1.40  
    1.41 -val locale_expr_unless = expr
    1.42 -val locale_expr = expr loc_keyword;
    1.43  val locale_keyword = loc_keyword;
    1.44  
    1.45  val locale_element = P.group "locale element"