src/Pure/General/path.scala

       else if (es.isEmpty) (List(Root("")), Nil)
       else (List(root_elem(es.head)), es.tail)
     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)
 
 
   /* encode */