# HG changeset patch
# User wenzelm
# Date 1309435411 -7200
# Node ID ff33fea12337e4470ad6f92ae7108bcd83e4d9b2
# Parent  8f777c2e4638eba589e2045ac4749c32d2b530da
more Path operations;
tuned signature;

diff -r 8f777c2e4638 -r ff33fea12337 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Jun 30 13:59:55 2011 +0200
+++ b/src/Pure/General/path.scala	Thu Jun 30 14:03:31 2011 +0200
@@ -102,19 +102,19 @@
   def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
 
-  def append(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
+  def +(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
 
 
-  /* print */
+  /* implode */
 
-  override def toString: String =
+  def implode: String =
     elems match {
       case Nil => "."
       case List(Path.Root("")) => "/"
-      case _ => elems.reverse.map(Path.implode_elem).mkString("/")
+      case _ => elems.map(Path.implode_elem).reverse.mkString("/")
     }
 
-  def print: String = Library.quote(toString)
+  override def toString: String = Library.quote(implode)
 
 
   /* base element */
@@ -122,7 +122,7 @@
   private def split_path: (Path, String) =
     elems match {
       case Path.Basic(s) :: xs => (Path(xs), s)
-      case _ => error("Cannot split path into dir/base: " + print)
+      case _ => error("Cannot split path into dir/base: " + toString)
     }
 
   def dir: Path = split_path._1
@@ -132,6 +132,20 @@
     if (e == "") this
     else {
       val (prfx, s) = split_path
-      prfx.append(Path.basic(s + "." + e))
+      prfx + Path.basic(s + "." + e)
     }
+
+
+  /* expand */
+
+  def expand(env: String => String): Path =
+  {
+    def eval(elem: Path.Elem): List[Path.Elem] =
+      elem match {
+        case Path.Variable(s) => Path.explode(env(s)).elems
+        case x => List(x)
+      }
+
+    Path(Path.norm_elems(elems.map(eval).flatten))
+  }
 }