proper File.standard_path for Windows: result of resources.source_file is platform_path (amending da1108a6d249);
--- a/src/Tools/VSCode/src/pretty_text_panel.scala Mon Feb 17 20:59:03 2025 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Tue Feb 18 17:16:55 2025 +0100
@@ -51,8 +51,8 @@
for {
thy_file <- Position.Def_File.unapply(props)
def_line <- Position.Def_Line.unapply(props)
- source <- resources.source_file(thy_file)
- uri = File.uri(Path.explode(source).absolute_file)
+ platform_path <- resources.source_file(thy_file)
+ uri = File.uri(Path.explode(File.standard_path(platform_path)).absolute_file)
} yield HTML.link(uri.toString + "#" + def_line, body)
}
val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full)