# HG changeset patch # User wenzelm # Date 1377034823 -7200 # Node ID 4c2b1e64c99056b1bc14cd9933e6ce8f51853be4 # Parent ae863ed9f64fc6b0b830da3e4f74e8775a82dbd0# Parent d9ba3417cb41d93801a1b8bdc525c40b7f34317f merged diff -r ae863ed9f64f -r 4c2b1e64c990 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Tue Aug 20 22:24:02 2013 +0200 +++ b/src/Pure/Isar/args.ML Tue Aug 20 23:40:23 2013 +0200 @@ -101,7 +101,8 @@ | Token.Typ T => Token.Typ (Morphism.typ phi T) | Token.Term t => Token.Term (Morphism.term phi t) | Token.Fact ths => Token.Fact (Morphism.fact phi ths) - | Token.Attribute att => Token.Attribute (Morphism.transform phi att))); + | Token.Attribute att => Token.Attribute (Morphism.transform phi att) + | tok as Token.Files _ => tok)); val assignable = map_args Token.assignable; val closure = map_args Token.closure; @@ -224,17 +225,25 @@ (* arguments within outer syntax *) +val argument_kinds = + [Token.Ident, Token.LongIdent, Token.SymIdent, Token.Var, Token.TypeIdent, Token.TypeVar, + Token.Nat, Token.Float, Token.String, Token.AltString, Token.Verbatim]; + fun parse_args is_symid = let - val keyword_symid = token (Parse.keyword_with is_symid); - fun atom blk = Parse.group (fn () => "argument") - (ident || keyword_symid || string || alt_string || token Parse.float_number || - (if blk then token (Parse.$$$ ",") else Scan.fail)); + fun argument blk = + Parse.group (fn () => "argument") + (Scan.one (fn tok => + let val kind = Token.kind_of tok in + member (op =) argument_kinds kind orelse + Token.keyword_with is_symid tok orelse + (blk andalso Token.keyword_with (fn s => s = ",") tok) + end)); fun args blk x = Scan.optional (args1 blk) [] x and args1 blk x = ((Scan.repeat1 - (Scan.repeat1 (atom blk) || + (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) >> flat) x and argsp l r x = diff -r ae863ed9f64f -r 4c2b1e64c990 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Tue Aug 20 22:24:02 2013 +0200 +++ b/src/Pure/Isar/bundle.ML Tue Aug 20 23:40:23 2013 +0200 @@ -61,7 +61,7 @@ let val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes; val bundle0 = raw_bundle - |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts)); + |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); val bundle = Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);