module OASISUnixPath:Unix path manipulationsig
..end
The filename and dirname used in '_oasis' file and OASISTypes.package
are
always encoded as Unix path. They are changed when using it on the target
system.
Author(s): Sylvain Le Gall
typeunix_filename =
string
typeunix_dirname =
unix_filename
typehost_filename =
string
typehost_dirname =
host_filename
val current_dir_name : unix_filename
val parent_dir_name : unix_filename
val concat : unix_filename ->
unix_filename -> unix_filename
concat fn1 fn2
Concatenate fn1 and fn2, i.e. fn1^'/'^fn2
.val make : unix_filename list -> unix_filename
make lst
Concatenate all filename components of lst
.val dirname : unix_filename -> unix_filename
dirname fn
Return directory name of fn
or current_dir_name
if no
directory name is defined.val basename : unix_filename -> unix_filename
basename fn
Return filename without its directory name.val chop_extension : unix_filename -> unix_filename
chop_extension fn
Remove the last part of the filename, after a '.',
return fn
if there is no extension.