# HG changeset patch
# User wenzelm
# Date 1421232728 -3600
# Node ID 4660b0409096a24338b429a7eec2d735c9b10d3b
# Parent  41f1645a4f63563420f8718b5c09db32133d97ee
added Path.decode in ML, in correspondence to Path.encode in Scala;

diff -r 41f1645a4f63 -r 4660b0409096 src/Pure/General/path.ML
--- 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 *)
 
diff -r 41f1645a4f63 -r 4660b0409096 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jan 13 21:46:09 2015 +0100
+++ b/src/Pure/ROOT.ML	Wed Jan 14 11:52:08 2015 +0100
@@ -65,6 +65,7 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
+use "PIDE/xml.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
@@ -78,7 +79,6 @@
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 use "General/sha1_samples.ML";
 
-use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";