src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Pure/General/url.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -8,6 +8,7 @@
 
 
 import java.io.{File => JFile}
+import java.nio.file.Paths
 import java.net.{URI, URISyntaxException}
 import java.net.{URL, MalformedURLException}
 import java.util.zip.GZIPInputStream
@@ -51,36 +52,15 @@
 
   /* file URIs */
 
-  def file(uri: String): JFile = new JFile(new URI(uri))
+  def print_file(file: JFile): String =
+    file.toPath.toAbsolutePath.toUri.normalize.toString
+
+  def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
 
   def is_wellformed_file(uri: String): Boolean =
-    try { file(uri); true }
+    try { parse_file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
 
   def normalize_file(uri: String): String =
-    if (is_wellformed_file(uri)) {
-      val uri1 = new URI(uri).normalize.toASCIIString
-      if (uri1.startsWith("file://")) uri1
-      else {
-        Library.try_unprefix("file:/", uri1) match {
-          case Some(p) => "file:///" + p
-          case None => uri1
-        }
-      }
-    }
-    else uri
-
-  def platform_file(path: Path): String =
-  {
-    val path1 = path.expand
-    require(path1.is_absolute)
-    platform_file(File.platform_path(path1))
-  }
-
-  def platform_file(name: String): String =
-    if (name.startsWith("file://")) name
-    else {
-      val s = name.replaceAll(" ", "%20")
-      "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
-    }
+    if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri
 }