--- a/src/Pure/General/url.scala Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/General/url.scala Fri Jun 30 14:19:37 2017 +0200
@@ -49,7 +49,7 @@
/* file URIs */
- def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString
+ def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
def print_file_name(name: String): String = print_file(new JFile(name))
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
@@ -61,6 +61,6 @@
false
}
- def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile
+ def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
def canonical_file_name(uri: String): String = canonical_file(uri).getPath
}