src/Pure/Isar/outer_parse.ML
changeset 12942 48fbe245879e
parent 12876 a70df1e5bf10
child 12955 f4d60f358cb6
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Mon Feb 25 20:51:00 2002 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Feb 25 20:51:27 2002 +0100
     1.3 @@ -68,7 +68,9 @@
     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_target: token list -> xstring option * token list
     1.8    val locale_expr: token list -> Locale.expr * token list
     1.9 +  val locale_keyword: token list -> string * token list
    1.10    val locale_element: token list -> Args.src Locale.element * token list
    1.11    val method: token list -> Method.text * token list
    1.12  end;
    1.13 @@ -309,7 +311,9 @@
    1.14  
    1.15  in
    1.16  
    1.17 +val locale_target = Scan.option (($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")"));
    1.18  val locale_expr = expr0;
    1.19 +val locale_keyword = loc_keyword;
    1.20  
    1.21  val locale_element = group "locale element"
    1.22    ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix