src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Mon Jan 02 18:08:04 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Jan 03 14:17:03 2017 +0100
@@ -57,6 +57,19 @@
     try { 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