# HG changeset patch
# User wenzelm
# Date 1492961018 -7200
# Node ID 7ff7781913a4fbb9ccaee0a568051b2677526e97
# Parent  479406635409fa882675b8d8d9657245e2ed2548
more operations;

diff -r 479406635409 -r 7ff7781913a4 src/Pure/General/mercurial.scala
--- 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 =
   {
diff -r 479406635409 -r 7ff7781913a4 src/Pure/General/path.scala
--- 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))