src/Tools/VSCode/src/pretty_text_panel.scala

           new Browser_Info.Node_Context {
             override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
               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)
         val html = node_context.make_html(elements, formatted)
         val message = output_json(HTML.source(html).toString, None)