1.1 --- a/src/Pure/General/path.scala	Thu Jun 30 13:59:55 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Thu Jun 30 14:03:31 2011 +0200
     1.3 @@ -102,19 +102,19 @@
     1.4    def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
     1.5    def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
     1.6  
     1.7 -  def append(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
     1.8 +  def +(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
     1.9  
    1.10  
    1.11 -  /* print */
    1.12 +  /* implode */
    1.13  
    1.14 -  override def toString: String =
    1.15 +  def implode: String =
    1.16      elems match {
    1.17        case Nil => "."
    1.18        case List(Path.Root("")) => "/"
    1.19 -      case _ => elems.reverse.map(Path.implode_elem).mkString("/")
    1.20 +      case _ => elems.map(Path.implode_elem).reverse.mkString("/")
    1.21      }
    1.22  
    1.23 -  def print: String = Library.quote(toString)
    1.24 +  override def toString: String = Library.quote(implode)
    1.25  
    1.26  
    1.27    /* base element */
    1.28 @@ -122,7 +122,7 @@
    1.29    private def split_path: (Path, String) =
    1.30      elems match {
    1.31        case Path.Basic(s) :: xs => (Path(xs), s)
    1.32 -      case _ => error("Cannot split path into dir/base: " + print)
    1.33 +      case _ => error("Cannot split path into dir/base: " + toString)
    1.34      }
    1.35  
    1.36    def dir: Path = split_path._1
    1.37 @@ -132,6 +132,20 @@
    1.38      if (e == "") this
    1.39      else {
    1.40        val (prfx, s) = split_path
    1.41 -      prfx.append(Path.basic(s + "." + e))
    1.42 +      prfx + Path.basic(s + "." + e)
    1.43      }
    1.44 +
    1.45 +
    1.46 +  /* expand */
    1.47 +
    1.48 +  def expand(env: String => String): Path =
    1.49 +  {
    1.50 +    def eval(elem: Path.Elem): List[Path.Elem] =
    1.51 +      elem match {
    1.52 +        case Path.Variable(s) => Path.explode(env(s)).elems
    1.53 +        case x => List(x)
    1.54 +      }
    1.55 +
    1.56 +    Path(Path.norm_elems(elems.map(eval).flatten))
    1.57 +  }
    1.58  }