proper platform_file_url for Windows UNC paths (server shares);
authorwenzelm
Wed Sep 28 13:52:14 2011 +0200 (2011-09-28 ago)
changeset 451016317e969fb30
parent 45100 0971c3ee3cdf
child 45102 7bb89635eb51
proper platform_file_url for Windows UNC paths (server shares);
src/Pure/System/isabelle_system.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:35:57 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Sep 28 13:52:14 2011 +0200
     1.3 @@ -114,10 +114,10 @@
     1.4    {
     1.5      val path = raw_path.expand
     1.6      require(path.is_absolute)
     1.7 -    val s =
     1.8 -      if (Platform.is_windows) "/" + platform_path(path).replace('\\', '/')
     1.9 -      else platform_path(path)
    1.10 -    "file://" + s.replaceAll(" ", "%20")
    1.11 +    val s = platform_path(path).replaceAll(" ", "%20")
    1.12 +    if (!Platform.is_windows) "file://" + s
    1.13 +    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
    1.14 +    else "file:///" + s.replace('\\', '/')
    1.15    }
    1.16  
    1.17    def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)