more informative position information;

--- a/src/Pure/General/position.ML	Wed May 10 20:38:24 2023 +0200
+++ b/src/Pure/General/position.ML	Wed May 10 21:17:21 2023 +0200
@@ -67,6 +67,7 @@
   val properties_of_range: range -> Properties.T
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
+  val setmp_thread_data_label: string -> ('a -> 'b) -> 'a -> 'b
   val default: T -> bool * T
 end;
 
@@ -319,6 +320,10 @@
 val thread_data = Pos o Thread_Position.get;
 fun setmp_thread_data pos = Thread_Position.setmp (dest pos);
 
+fun setmp_thread_data_label a f x =
+  if a = "" then f x
+  else setmp_thread_data (label a (thread_data ())) f x;
+
 fun default pos =
   if pos = none then (false, thread_data ())
   else (true, pos);

--- a/src/Pure/Isar/attrib.ML	Wed May 10 20:38:24 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed May 10 21:17:21 2023 +0200
@@ -163,8 +163,14 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val table = Attributes.get context
-  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
+  let val table = Attributes.get context in
+    fn src =>
+      let
+        val name = #1 (Token.name_of_src src);
+        val label = Long_Name.qualify Markup.attributeN name;
+        val att = #1 (Name_Space.get table name) src;
+      in Position.setmp_thread_data_label label att end
+  end;
 
 val attribute = attribute_generic o Context.Proof;
 val attribute_global = attribute_generic o Context.Theory;