src/Pure/Thy/thy_info.ML
changeset 78021 ce6e3bc34343
parent 77889 5db014c36f42
child 78527 374611eb3055
--- a/src/Pure/Thy/thy_info.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 10 20:30:46 2023 +0200
@@ -44,7 +44,7 @@
     val props' = Position.properties_of (#adjust_pos context pos);
   in
     filter (fn (a, _) => a = Markup.offsetN orelse a = Markup.end_offsetN) props' @
-    filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) props
+    filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN) props
   end;
 
 structure Presentation = Theory_Data