# 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)