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)