changeset 76880 | 6a07cf09604d |
parent 76432 | d0079b509d99 |
child 76884 | a004c5322ea4 |
--- a/src/Pure/Thy/thy_info.ML Tue Jan 03 12:58:00 2023 +0100 +++ b/src/Pure/Thy/thy_info.ML Tue Jan 03 14:00:59 2023 +0100 @@ -326,7 +326,7 @@ Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ id); - val text_pos = put_id (Path.position thy_path); + val text_pos = put_id (Position.file (Path.implode_symbolic thy_path)); val text_props = Position.properties_of text_pos; val _ = remove_thy name;