src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Mon Mar 03 11:37:06 2014 +0100
+++ b/src/Pure/General/path.scala	Mon Mar 03 11:58:07 2014 +0100
@@ -97,9 +97,12 @@
     new Path(norm_elems(elems.reverse ::: roots))
   }
 
-  def is_ok(str: String): Boolean =
+  def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }
 
+  def is_valid(str: String): Boolean =
+    try { explode(str).expand; true } catch { case ERROR(_) => false }
+
   def split(str: String): List[Path] =
     space_explode(':', str).filterNot(_.isEmpty).map(explode)