--- a/src/Pure/General/mercurial.scala Sun Apr 23 16:18:31 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sun Apr 23 17:23:38 2017 +0200
@@ -35,6 +35,19 @@
hg
}
+ def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] =
+ {
+ def find(root: Path): Option[Repository] =
+ if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
+ else if (root.is_root) None
+ else find(root + Path.parent)
+
+ ssh match {
+ case None => find(start.expand)
+ case Some(ssh) => find(ssh.expand_path(start))
+ }
+ }
+
def clone_repository(
source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
{
--- a/src/Pure/General/path.scala Sun Apr 23 16:18:31 2017 +0200
+++ b/src/Pure/General/path.scala Sun Apr 23 17:23:38 2017 +0200
@@ -119,6 +119,7 @@
{
def is_current: Boolean = elems.isEmpty
def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
+ def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))