src/Pure/General/url.scala
changeset 66234 836898197296
parent 65188 50cfc6775361
child 66235 d4fa51e7c4ff
--- 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
 }