diff -r cdb0d559a24b -r 39a6c88c059b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Dec 23 19:19:59 2016 +0100
+++ b/src/Pure/General/file.scala	Fri Dec 23 20:06:54 2016 +0100
@@ -99,12 +99,18 @@
   {
     val path = raw_path.expand
     require(path.is_absolute)
-    val s = platform_path(path).replaceAll(" ", "%20")
-    if (!Platform.is_windows) "file://" + s
-    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-    else "file:///" + s.replace('\\', '/')
+    platform_url(platform_path(path))
   }
 
+  def platform_url(name: String): String =
+    if (name.startsWith("file://")) name
+    else {
+      val s = name.replaceAll(" ", "%20")
+      if (!Platform.is_windows) "file://" + s
+      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+      else "file:///" + s.replace('\\', '/')
+    }
+
 
   /* bash path */