413 val commas_quote = commas o map quote; |
413 val commas_quote = commas o map quote; |
414 |
414 |
415 (*concatenate messages, one per line, into a string*) |
415 (*concatenate messages, one per line, into a string*) |
416 val cat_lines = space_implode "\n"; |
416 val cat_lines = space_implode "\n"; |
417 |
417 |
|
418 (*space_explode "." "h.e..l.lo"; gives ["h", "e", "l", "lo"]*) |
|
419 fun space_explode sep s = |
|
420 let fun divide [] "" = [] |
|
421 | divide [] part = [part] |
|
422 | divide (c::s) part = |
|
423 if c = sep then |
|
424 (if part = "" then divide s "" else part :: divide s "") |
|
425 else divide s (part ^ c) |
|
426 in divide (explode s) "" end; |
418 |
427 |
419 |
428 |
420 (** lists as sets **) |
429 (** lists as sets **) |
421 |
430 |
422 (*membership in a list*) |
431 (*membership in a list*) |
696 fun exit_use fname = use fname handle _ => exit 1; |
705 fun exit_use fname = use fname handle _ => exit 1; |
697 |
706 |
698 |
707 |
699 (** filenames **) |
708 (** filenames **) |
700 |
709 |
701 (*convert UNIX filename of the form "path/file" to "path/" and "file"; |
710 (*Convert UNIX filename of the form "path/file" to "path/" and "file"; |
702 if filename contains no slash, then it returns "" and "file"*) |
711 if filename contains no slash, then it returns "" and "file"*) |
703 val split_filename = |
712 val split_filename = |
704 (pairself implode) o take_suffix (not_equal "/") o explode; |
713 (pairself implode) o take_suffix (not_equal "/") o explode; |
705 |
714 |
706 val base_name = #2 o split_filename; |
715 val base_name = #2 o split_filename; |
707 |
716 |
708 (*merge splitted filename (path and file); |
717 (*Merge splitted filename (path and file); |
709 if path does not end with one a slash is appended*) |
718 if path does not end with one a slash is appended*) |
710 fun tack_on "" name = name |
719 fun tack_on "" name = name |
711 | tack_on path name = |
720 | tack_on path name = |
712 if last_elem (explode path) = "/" then path ^ name |
721 if last_elem (explode path) = "/" then path ^ name |
713 else path ^ "/" ^ name; |
722 else path ^ "/" ^ name; |
714 |
723 |
715 (*remove the extension of a filename, i.e. the part after the last '.'*) |
724 (*Remove the extension of a filename, i.e. the part after the last '.'*) |
716 val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode; |
725 val remove_ext = implode o #1 o take_suffix (not_equal ".") o explode; |
717 |
726 |
|
727 (*Make relative path to reach an absolute location from a different one*) |
|
728 fun relative_path cur_path dest_path = |
|
729 let (*Remove common beginning of both paths and make relative path*) |
|
730 fun mk_relative [] [] = [] |
|
731 | mk_relative [] ds = ds |
|
732 | mk_relative cs [] = map (fn _ => "..") cs |
|
733 | mk_relative (c::cs) (d::ds) = |
|
734 if c = d then mk_relative cs ds |
|
735 else ".." :: map (fn _ => "..") cs @ (d::ds); |
|
736 in if cur_path = "" orelse hd (explode cur_path) <> "/" orelse |
|
737 dest_path = "" orelse hd (explode dest_path) <> "/" then |
|
738 error "Relative or empty path passed to relative_path" |
|
739 else (); |
|
740 space_implode "/" (mk_relative (space_explode "/" cur_path) |
|
741 (space_explode "/" dest_path)) |
|
742 end; |
718 |
743 |
719 |
744 |
720 (** misc functions **) |
745 (** misc functions **) |
721 |
746 |
722 (*use the keyfun to make a list of (x, key) pairs*) |
747 (*use the keyfun to make a list of (x, key) pairs*) |