src/Pure/Isar/attrib.ML
changeset 47816 cd0dfb06b0c8
parent 47815 43f677b3ae91
child 48205 09c2a3d9aa22
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 27 22:47:30 2012 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 27 22:58:29 2012 +0200
     1.3 @@ -122,22 +122,24 @@
     1.4  
     1.5  val defined = Symtab.defined o #2 o Attributes.get;
     1.6  
     1.7 -fun attribute_global thy =
     1.8 +fun attribute_generic context =
     1.9    let
    1.10 +    val thy = Context.theory_of context;
    1.11      val (space, tab) = Attributes.get thy;
    1.12      fun attr src =
    1.13        let val ((name, _), pos) = Args.dest_src src in
    1.14          (case Symtab.lookup tab name of
    1.15            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    1.16 -        | SOME (att, _) => (Position.report pos (Name_Space.markup space name); att src))
    1.17 +        | SOME (att, _) =>
    1.18 +            (Context_Position.report_generic context pos (Name_Space.markup space name); att src))
    1.19        end;
    1.20    in attr end;
    1.21  
    1.22 -val attribute = attribute_global o Proof_Context.theory_of;
    1.23 -val attribute_generic = attribute_global o Context.theory_of;
    1.24 +val attribute = attribute_generic o Context.Proof;
    1.25 +val attribute_global = attribute_generic o Context.Theory;
    1.26  
    1.27 +fun attribute_cmd ctxt = attribute ctxt o intern_src (Proof_Context.theory_of ctxt);
    1.28  fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
    1.29 -val attribute_cmd = attribute_cmd_global o Proof_Context.theory_of;
    1.30  
    1.31  
    1.32  (* attributed declarations *)