proper platform_file_url for Windows UNC paths (server shares);
authorwenzelm
Wed, 28 Sep 2011 13:52:14 +0200
changeset 45101 6317e969fb30
parent 45100 0971c3ee3cdf
child 45102 7bb89635eb51
proper platform_file_url for Windows UNC paths (server shares);
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:35:57 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Sep 28 13:52:14 2011 +0200
@@ -114,10 +114,10 @@
   {
     val path = raw_path.expand
     require(path.is_absolute)
-    val s =
-      if (Platform.is_windows) "/" + platform_path(path).replace('\\', '/')
-      else platform_path(path)
-    "file://" + s.replaceAll(" ", "%20")
+    val s = platform_path(path).replaceAll(" ", "%20")
+    if (!Platform.is_windows) "file://" + s
+    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+    else "file:///" + s.replace('\\', '/')
   }
 
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)