[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")