# HG changeset patch
# User wenzelm
# Date 1335560309 -7200
# Node ID cd0dfb06b0c89f3db9ca7aadeb86a82ee27f2bcc
# Parent  43f677b3ae91ff2126f936c83ab2a8704e708026
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;

diff -r 43f677b3ae91 -r cd0dfb06b0c8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 27 22:47:30 2012 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 27 22:58:29 2012 +0200
@@ -122,22 +122,24 @@
 
 val defined = Symtab.defined o #2 o Attributes.get;
 
-fun attribute_global thy =
+fun attribute_generic context =
   let
+    val thy = Context.theory_of context;
     val (space, tab) = Attributes.get thy;
     fun attr src =
       let val ((name, _), pos) = Args.dest_src src in
         (case Symtab.lookup tab name of
           NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
-        | SOME (att, _) => (Position.report pos (Name_Space.markup space name); att src))
+        | SOME (att, _) =>
+            (Context_Position.report_generic context pos (Name_Space.markup space name); att src))
       end;
   in attr end;
 
-val attribute = attribute_global o Proof_Context.theory_of;
-val attribute_generic = attribute_global o Context.theory_of;
+val attribute = attribute_generic o Context.Proof;
+val attribute_global = attribute_generic o Context.Theory;
 
+fun attribute_cmd ctxt = attribute ctxt o intern_src (Proof_Context.theory_of ctxt);
 fun attribute_cmd_global thy = attribute_global thy o intern_src thy;
-val attribute_cmd = attribute_cmd_global o Proof_Context.theory_of;
 
 
 (* attributed declarations *)