--- 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;