src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/General/path.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -96,6 +96,9 @@
     new Path(norm_elems(explode_elems(raw_elems) ++ roots))
   }
 
+  def is_ok(str: String): Boolean =
+    try { explode(str); true } catch { case ERROR(_) => false }
+
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)