prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
authorwenzelm
Fri, 27 Apr 2012 22:58:29 +0200
changeset 47816 cd0dfb06b0c8
parent 47815 43f677b3ae91
child 47817 5d2d63f4363e
prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;
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 *)