--- 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)