src/Pure/Thy/thy_info.ML
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;