added for_simple_fixes, specification;
authorwenzelm
Tue Nov 14 22:17:03 2006 +0100 (2006-11-14)
changeset 213716717630f080b
parent 21370 d9dd7b4e5e69
child 21372 4a0a83378669
added for_simple_fixes, specification;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Nov 14 22:17:01 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Nov 14 22:17:03 2006 +0100
     1.3 @@ -66,6 +66,7 @@
     1.4    val simple_fixes: token list -> (string * string option) list * token list
     1.5    val fixes: token list -> (string * string option * mixfix) list * token list
     1.6    val for_fixes: token list -> (string * string option * mixfix) list * token list
     1.7 +  val for_simple_fixes: token list -> (string * string option) list * token list
     1.8    val term: token list -> string * token list
     1.9    val prop: token list -> string * token list
    1.10    val propp: token list -> (string * string list) * token list
    1.11 @@ -90,8 +91,8 @@
    1.12    val locale_target: token list -> xstring * token list
    1.13    val opt_locale_target: token list -> xstring option * token list
    1.14    val locale_expr: token list -> Locale.expr * token list
    1.15 -  val locale_expr_unless: (token list -> 'a * token list) -> 
    1.16 -         token list -> Locale.expr * token list 
    1.17 +  val locale_expr_unless: (token list -> 'a * token list) ->
    1.18 +    token list -> Locale.expr * token list
    1.19    val locale_keyword: token list -> string * token list
    1.20    val locale_element: token list -> Element.context Locale.element * token list
    1.21    val context_element: token list -> Element.context * token list
    1.22 @@ -100,6 +101,10 @@
    1.23    val general_statement: token list ->
    1.24      (Element.context Locale.element list * Element.statement) * OuterLex.token list
    1.25    val statement_keyword: token list -> string * token list
    1.26 +  val specification: token list ->
    1.27 +    (string *
    1.28 +      (((bstring * Attrib.src list) * string list) list * (string * string option) list)) list *
    1.29 +    token list
    1.30    val method: token list -> Method.text * token list
    1.31  end;
    1.32  
    1.33 @@ -274,6 +279,7 @@
    1.34      params >> map Syntax.no_syn) >> flat;
    1.35  
    1.36  val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
    1.37 +val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
    1.38  
    1.39  
    1.40  (* terms *)
    1.41 @@ -381,7 +387,7 @@
    1.42  val rename = name -- Scan.option mixfix;
    1.43  
    1.44  fun expr test =
    1.45 -  let 
    1.46 +  let
    1.47      fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
    1.48      and expr1 x = (expr2 -- Scan.repeat1 (maybe rename) >> Locale.Rename || expr2) x
    1.49      and expr0 x = (plus1 test expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.50 @@ -419,6 +425,11 @@
    1.51  val statement_keyword =  $$$ "obtains" || $$$ "shows";
    1.52  
    1.53  
    1.54 +(* specifications *)
    1.55 +
    1.56 +val specification = enum1 "|" (parname -- (and_list1 spec -- for_simple_fixes));
    1.57 +
    1.58 +
    1.59  (* proof methods *)
    1.60  
    1.61  fun is_symid_meth s =