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