# HG changeset patch
# User wenzelm
# Date 1506435141 -7200
# Node ID 02588021b5811e1c5e2c918a933cf44bb24c92ca
# Parent  ef81649ad05105f1fdd7e402dcace997559437a2
more operations;

diff -r ef81649ad051 -r 02588021b581 src/Pure/General/file.scala
--- 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))