src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Mon Jul 23 22:35:10 2012 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 24 00:29:36 2012 +0200
@@ -98,6 +98,11 @@
 
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)
+
+
+  /* encode */
+
+  val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
 }