--- a/src/Pure/General/file.scala Mon Sep 25 09:46:26 2017 +0200
+++ b/src/Pure/General/file.scala Tue Sep 26 16:12:21 2017 +0200
@@ -106,6 +106,21 @@
def pwd(): Path = path(Path.current.absolute_file)
+ /* relative paths */
+
+ def relative_path(base: Path, other: Path): Option[Path] =
+ {
+ val base_path = base.file.toPath
+ val other_path = other.file.toPath
+ if (other_path.startsWith(base_path))
+ Some(path(base_path.relativize(other_path).toFile))
+ else None
+ }
+
+ def rebase_path(base: Path, other: Path): Option[Path] =
+ relative_path(base, other).map(base + _)
+
+
/* bash path */
def bash_path(path: Path): String = Bash.string(standard_path(path))