# HG changeset patch # User clasohm # Date 814538466 -3600 # Node ID ee8f41456d288c0989d9c7cf2e783d1e6dc7a5dd # Parent 2edd7a39d92a6a27e7a0a39d24c8bf10fcdc95f1 added space_explode and relative_path diff -r 2edd7a39d92a -r ee8f41456d28 src/Pure/library.ML --- a/src/Pure/library.ML Tue Oct 24 13:40:06 1995 +0100 +++ b/src/Pure/library.ML Tue Oct 24 13:41:06 1995 +0100 @@ -415,6 +415,15 @@ (*concatenate messages, one per line, into a string*) val cat_lines = space_implode "\n"; +(*space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*) +fun space_explode sep s = + let fun divide [] "" = [] + | divide [] part = [part] + | divide (c::s) part = + if c = sep then + (if part = "" then divide s "" else part :: divide s "") + else divide s (part ^ c) + in divide (explode s) "" end; (** lists as sets **) @@ -698,23 +707,39 @@ (** filenames **) -(*convert UNIX filename of the form "path/file" to "path/" and "file"; +(*Convert UNIX filename of the form "path/file" to "path/" and "file"; if filename contains no slash, then it returns "" and "file"*) val split_filename = (pairself implode) o take_suffix (not_equal "/") o explode; val base_name = #2 o split_filename; -(*merge splitted filename (path and file); +(*Merge splitted filename (path and file); if path does not end with one a slash is appended*) fun tack_on "" name = name | tack_on path name = if last_elem (explode path) = "/" then path ^ name else path ^ "/" ^ name; -(*remove the extension of a filename, i.e. the part after the last '.'*) +(*Remove the extension of a filename, i.e. the part after the last '.'*) val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode; +(*Make relative path to reach an absolute location from a different one*) +fun relative_path cur_path dest_path = + let (*Remove common beginning of both paths and make relative path*) + fun mk_relative [] [] = [] + | mk_relative [] ds = ds + | mk_relative cs [] = map (fn _ => "..") cs + | mk_relative (c::cs) (d::ds) = + if c = d then mk_relative cs ds + else ".." :: map (fn _ => "..") cs @ (d::ds); + in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse + dest_path = "" orelse hd (explode dest_path) <> "/" then + error "Relative or empty path passed to relative_path" + else (); + space_implode "/" (mk_relative (space_explode "/" cur_path) + (space_explode "/" dest_path)) + end; (** misc functions **)