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 decode: T XML.Decode.T
   val split: string -> T list
   val pretty: T -> Pretty.T
   val print: T -> string
   val dir: T -> T
   val base: T -> T

   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));
+
+val decode = XML.Decode.string #> explode_path;
 
 
 (* print *)
 
 fun pretty path =