added space_explode and relative_path
authorclasohm
Tue Oct 24 13:41:06 1995 +0100 (1995-10-24)
changeset 1290ee8f41456d28
parent 1289 2edd7a39d92a
child 1291 e173be970d27
added space_explode and relative_path
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Oct 24 13:40:06 1995 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Oct 24 13:41:06 1995 +0100
     1.3 @@ -415,6 +415,15 @@
     1.4  (*concatenate messages, one per line, into a string*)
     1.5  val cat_lines = space_implode "\n";
     1.6  
     1.7 +(*space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*)
     1.8 +fun space_explode sep s =
     1.9 +  let fun divide [] "" = []
    1.10 +        | divide [] part = [part]
    1.11 +        | divide (c::s) part =
    1.12 +            if c = sep then
    1.13 +              (if part = "" then divide s "" else part :: divide s "")
    1.14 +            else divide s (part ^ c)
    1.15 +  in divide (explode s) "" end;
    1.16  
    1.17  
    1.18  (** lists as sets **)
    1.19 @@ -698,23 +707,39 @@
    1.20  
    1.21  (** filenames **)
    1.22  
    1.23 -(*convert UNIX filename of the form "path/file" to "path/" and "file";
    1.24 +(*Convert UNIX filename of the form "path/file" to "path/" and "file";
    1.25    if filename contains no slash, then it returns "" and "file"*)
    1.26  val split_filename =
    1.27    (pairself implode) o take_suffix (not_equal "/") o explode;
    1.28  
    1.29  val base_name = #2 o split_filename;
    1.30  
    1.31 -(*merge splitted filename (path and file);
    1.32 +(*Merge splitted filename (path and file);
    1.33    if path does not end with one a slash is appended*)
    1.34  fun tack_on "" name = name
    1.35    | tack_on path name =
    1.36        if last_elem (explode path) = "/" then path ^ name
    1.37        else path ^ "/" ^ name;
    1.38  
    1.39 -(*remove the extension of a filename, i.e. the part after the last '.'*)
    1.40 +(*Remove the extension of a filename, i.e. the part after the last '.'*)
    1.41  val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode;
    1.42  
    1.43 +(*Make relative path to reach an absolute location from a different one*)
    1.44 +fun relative_path cur_path dest_path =
    1.45 +  let (*Remove common beginning of both paths and make relative path*)
    1.46 +      fun mk_relative [] [] = []
    1.47 +        | mk_relative [] ds = ds
    1.48 +        | mk_relative cs [] = map (fn _ => "..") cs
    1.49 +        | mk_relative (c::cs) (d::ds) =
    1.50 +            if c = d then mk_relative cs ds
    1.51 +            else ".." :: map (fn _ => "..") cs @ (d::ds);
    1.52 +  in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse
    1.53 +        dest_path = "" orelse hd (explode dest_path) <> "/" then
    1.54 +       error "Relative or empty path passed to relative_path"
    1.55 +     else ();
    1.56 +     space_implode "/" (mk_relative (space_explode "/" cur_path)
    1.57 +                                    (space_explode "/" dest_path))
    1.58 +  end;
    1.59  
    1.60  
    1.61  (** misc functions **)