src/Pure/General/url.scala

--- a/src/Pure/General/url.scala	Sun Jan 01 11:38:29 2017 +0100
+++ b/src/Pure/General/url.scala	Sun Jan 01 11:47:27 2017 +0100
@@ -56,4 +56,20 @@
   def is_wellformed_file(uri: String): Boolean =
     try { file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
+
+  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")
+      if (!Platform.is_windows) "file://" + s
+      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+      else "file:///" + s.replace('\\', '/')
+    }
 }