# HG changeset patch
# User wenzelm
# Date 1675674235 -3600
# Node ID 2cf7a61e4a73b8a0b3a4230d8cb3adf0ab4ad1e7
# Parent  7d7786585ab0d8dbd7ce56d8b5361c2d5e3a4401
clarified signature;

diff -r 7d7786585ab0 -r 2cf7a61e4a73 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/Pure/General/file.scala	Mon Feb 06 10:03:55 2023 +0100
@@ -75,10 +75,7 @@
   /* platform files */
 
   def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
-  def absolute_name(file: JFile): String = absolute(file).getPath
-
   def canonical(file: JFile): JFile = file.getCanonicalFile
-  def canonical_name(file: JFile): String = canonical(file).getPath
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def path(java_path: JPath): Path = path(java_path.toFile)
diff -r 7d7786585ab0 -r 2cf7a61e4a73 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Feb 05 20:09:39 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Feb 06 10:03:55 2023 +0100
@@ -107,7 +107,7 @@
     else if (path.is_basic && !prefix.endsWith("/") && !prefix.endsWith(JFile.separator))
       prefix + JFile.separator + File.platform_path(path)
     else if (path.is_basic) prefix + File.platform_path(path)
-    else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path)))
+    else File.absolute(new JFile(prefix + JFile.separator + File.platform_path(path))).getPath
   }
 
   override def read_dir(dir: String): List[String] =