src/Pure/General/path.ML

   val append: T -> T -> T
   val appends: T list -> T
   val make: string list -> T
   val implode: T -> string
   val explode: string -> T
+  val split: string -> T list
   val pretty: T -> Pretty.T
   val print: T -> string
   val dir: T -> T
   val base: T -> T
   val ext: string -> T -> T

       | (_, e :: es) => ([root_elem e], es));
     val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem;
 
   in Path (norm (rev elems @ roots)) end;
 
+fun split str =
+  space_explode ":" str
+  |> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
+
 
 (* print *)
 
 fun pretty path =
   let val s = implode_path path