# HG changeset patch
# User wenzelm
# Date 1739895415 -3600
# Node ID 7dc4aa4078995736384e6cd666245dea5e216e17
# Parent  3c88bec13e60cb7819f91f9effc6bf99a4140094
proper File.standard_path for Windows: result of resources.source_file is platform_path (amending da1108a6d249);

diff -r 3c88bec13e60 -r 7dc4aa407899 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)