don't register "sequential" as a keyword for now as this breaks the parser for function
authortraytel
Sun Sep 08 12:26:05 2013 +0200 (2013-09-08)
changeset 534693356a148b783
parent 53468 0688928a41fd
child 53470 fe80dd7cd543
don't register "sequential" as a keyword for now as this breaks the parser for function
etc/isar-keywords.el
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Tools/bnf_gfp.ML
     1.1 --- a/etc/isar-keywords.el	Sat Sep 07 23:09:26 2013 +0200
     1.2 +++ b/etc/isar-keywords.el	Sun Sep 08 12:26:05 2013 +0200
     1.3 @@ -350,7 +350,6 @@
     1.4      "permissive"
     1.5      "pervasive"
     1.6      "rep_compat"
     1.7 -    "sequential"
     1.8      "shows"
     1.9      "structure"
    1.10      "type_class"
     2.1 --- a/src/HOL/BNF/BNF_GFP.thy	Sat Sep 07 23:09:26 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Sun Sep 08 12:26:05 2013 +0200
     2.3 @@ -11,8 +11,7 @@
     2.4  imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
     2.5  keywords
     2.6    "codatatype" :: thy_decl and
     2.7 -  "primcorec" :: thy_goal and
     2.8 -  "sequential"
     2.9 +  "primcorec" :: thy_goal
    2.10  begin
    2.11  
    2.12  lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sat Sep 07 23:09:26 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 08 12:26:05 2013 +0200
     3.3 @@ -2903,9 +2903,17 @@
     3.4    Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     3.5      (parse_co_datatype_cmd Greatest_FP construct_gfp);
     3.6  
     3.7 +local
     3.8 +
     3.9 +val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
    3.10 +
    3.11 +in
    3.12 +
    3.13  val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
    3.14    "define primitive corecursive functions"
    3.15 -  ((Scan.option @{keyword "sequential"} >> is_some) --
    3.16 +  ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    3.17      (Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
    3.18 + 
    3.19 +end
    3.20  
    3.21  end;