proper File.standard_path for Windows: result of resources.source_file is platform_path (amending da1108a6d249);
authorwenzelm
Tue, 18 Feb 2025 17:16:55 +0100
changeset 82192 7dc4aa407899
parent 82191 3c88bec13e60
child 82193 355a2c1cdf40
proper File.standard_path for Windows: result of resources.source_file is platform_path (amending da1108a6d249);
src/Tools/VSCode/src/pretty_text_panel.scala
--- 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)