# HG changeset patch
# User wenzelm
# Date 1483467737 -3600
# Node ID 6fd05caf55f0ede8f337389b2fc5e2476975b242
# Parent  8ae1af3f88b1c453fd5d47eb85b614f0d5d60f8e
clarified file URLs, notably for Windows UNC paths;

diff -r 8ae1af3f88b1 -r 6fd05caf55f0 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Jan 03 17:33:08 2017 +0100
+++ b/src/Pure/General/url.scala	Tue Jan 03 19:22:17 2017 +0100
@@ -81,8 +81,6 @@
     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('\\', '/')
+      "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
     }
 }
diff -r 8ae1af3f88b1 -r 6fd05caf55f0 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 17:33:08 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 19:22:17 2017 +0100
@@ -50,8 +50,8 @@
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
-    if (path.is_absolute) "file://" + path.implode
-    else if (dir == "") "file://" + (File.pwd() + path).implode
+    if (path.is_absolute) Url.platform_file(path)
+    else if (dir == "") Url.platform_file(File.pwd() + path)
     else if (path.is_current) dir
     else Url.normalize_file(dir + "/" + path.implode)
   }