diff -r 186e07be32c3 -r a004c5322ea4 src/Tools/Code/code_target.ML
--- 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;