src/Pure/Isar/args.ML
changeset 42464 ae16b8abf1a8
parent 42360 da8817d01e7c
child 44357 5f5649ac8235
     1.1 --- a/src/Pure/Isar/args.ML	Sat Apr 23 13:00:19 2011 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Sat Apr 23 13:53:09 2011 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4    val named_typ: (string -> typ) -> typ parser
     1.5    val named_term: (string -> term) -> term parser
     1.6    val named_fact: (string -> thm list) -> thm list parser
     1.7 -  val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
     1.8 +  val named_attribute:
     1.9 +    (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
    1.10    val typ_abbrev: typ context_parser
    1.11    val typ: typ context_parser
    1.12    val term: term context_parser
    1.13 @@ -176,10 +177,13 @@
    1.14  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    1.15  fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
    1.16  fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
    1.17 +
    1.18  fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
    1.19    alt_string >> evaluate Token.Fact (get o Token.source_of);
    1.20 +
    1.21  fun named_attribute att =
    1.22 -  internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
    1.23 +  internal_attribute ||
    1.24 +  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok));
    1.25  
    1.26  
    1.27  (* terms and types *)