[MLton] Windows ports and paths

Andreas Rossberg AndreasRossberg@web.de
Mon, 2 May 2005 22:41:55 +0200


> * joinDirFile should not trim the slash from the directory.

But doesn't your code do precisly the opposite?

>  So, it should look something like 
> 
>     fun endsInSlash s = slash sub 0 = String.sub (s, size s - 1)
> 
>     fun joinDirFile {dir, file} =
>        if not (isArc file) then raise InvalidArc
>        else if 0 = size dir then file
>        else if endsInSlash dir then String.concat [dir, file]
>        else String.concat [dir, slash, file]

I think the proper implementation simply is

    fun joinDirFile {dir, file} =
       if not (isArc file) then raise InvalidArc
       else if 0 = size dir then file
       else String.concat [dir, slash, file]

This gives

  joinDirFile("","b") = "b"
  joinDirFile("b","") = "b/"
  joinDirFile("b","c") = "b/c"
  joinDirFile("b/","c") = "b//c"

which is consistent with

  splitDirFile "b" = ("","b")
  splitDirFile "b/" = ("b","")
  splitDirFile "b/c" = ("b","c")
  splitDirFile "b//c" = ("b/","c")