# HG changeset patch
# User wenzelm
# Date 1660915479 -7200
# Node ID 6d9d9a395533ef1132ca27c518760d30d67f8d52
# Parent  dce94a1d18fd88e1bd57d6291d4d987ee5c97c4a
export entity file position as well, e.g. relevant for HTML presentation with aux. files;

diff -r dce94a1d18fd -r 6d9d9a395533 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 19 15:06:04 2022 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 19 15:24:39 2022 +0200
@@ -38,7 +38,8 @@
     segments: Document_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
-  Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
+  Position.offset_properties_of (#adjust_pos context pos) @
+  filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.get_props pos);
 
 structure Presentation = Theory_Data
 (