--- a/src/Pure/General/path.ML Tue Jan 13 21:46:09 2015 +0100
+++ b/src/Pure/General/path.ML Wed Jan 14 11:52:08 2015 +0100
@@ -23,6 +23,7 @@
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
@@ -161,6 +162,8 @@
space_explode ":" str
|> map_filter (fn s => if s = "" then NONE else SOME (explode_path s));
+val decode = XML.Decode.string #> explode_path;
+
(* print *)