src/Pure/General/file.scala
changeset 64668 39a6c88c059b
parent 64482 43f6c28ff496
child 64698 e022a69db531
equal deleted inserted replaced
64667:cdb0d559a24b 64668:39a6c88c059b
    97 
    97 
    98   def platform_url(raw_path: Path): String =
    98   def platform_url(raw_path: Path): String =
    99   {
    99   {
   100     val path = raw_path.expand
   100     val path = raw_path.expand
   101     require(path.is_absolute)
   101     require(path.is_absolute)
   102     val s = platform_path(path).replaceAll(" ", "%20")
   102     platform_url(platform_path(path))
   103     if (!Platform.is_windows) "file://" + s
   103   }
   104     else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
   104 
   105     else "file:///" + s.replace('\\', '/')
   105   def platform_url(name: String): String =
   106   }
   106     if (name.startsWith("file://")) name
       
   107     else {
       
   108       val s = name.replaceAll(" ", "%20")
       
   109       if (!Platform.is_windows) "file://" + s
       
   110       else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
       
   111       else "file:///" + s.replace('\\', '/')
       
   112     }
   107 
   113 
   108 
   114 
   109   /* bash path */
   115   /* bash path */
   110 
   116 
   111   def bash_path(path: Path): String = Bash.string(standard_path(path))
   117   def bash_path(path: Path): String = Bash.string(standard_path(path))