more operations;
authorwenzelm
Tue Sep 26 16:12:21 2017 +0200 (21 months ago)
changeset 6669302588021b581
parent 66689 ef81649ad051
child 66694 41177b124067
more operations;
src/Pure/General/file.scala
     1.1 --- a/src/Pure/General/file.scala	Mon Sep 25 09:46:26 2017 +0200
     1.2 +++ b/src/Pure/General/file.scala	Tue Sep 26 16:12:21 2017 +0200
     1.3 @@ -106,6 +106,21 @@
     1.4    def pwd(): Path = path(Path.current.absolute_file)
     1.5  
     1.6  
     1.7 +  /* relative paths */
     1.8 +
     1.9 +  def relative_path(base: Path, other: Path): Option[Path] =
    1.10 +  {
    1.11 +    val base_path = base.file.toPath
    1.12 +    val other_path = other.file.toPath
    1.13 +    if (other_path.startsWith(base_path))
    1.14 +      Some(path(base_path.relativize(other_path).toFile))
    1.15 +    else None
    1.16 +  }
    1.17 +
    1.18 +  def rebase_path(base: Path, other: Path): Option[Path] =
    1.19 +    relative_path(base, other).map(base + _)
    1.20 +
    1.21 +
    1.22    /* bash path */
    1.23  
    1.24    def bash_path(path: Path): String = Bash.string(standard_path(path))