--- a/src/Tools/Code/code_target.ML Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Tools/Code/code_target.ML Tue Jan 03 16:05:07 2023 +0100
@@ -541,7 +541,7 @@
Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
val _ = Position.report pos (Markup.language_path delimited);
val path = #1 (Path.explode_pos (s, pos));
- val _ = Position.report pos (Markup.path (Path.implode_symbolic path));
+ val _ = Position.report pos (Markup.path (File.symbolic_path path));
in (location, (path, pos)) end
end;