# HG changeset patch
# User wenzelm
# Date 1716563217 -7200
# Node ID e8d4ac2f21ea91805e6ccc398997f25a9493dceb
# Parent  3956e8b6a9c90cb86e90834a06465beb1a050c69
clarified modules;

diff -r 3956e8b6a9c9 -r e8d4ac2f21ea src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Fri May 24 16:15:27 2024 +0200
+++ b/src/Pure/General/mercurial.scala	Fri May 24 17:06:57 2024 +0200
@@ -172,15 +172,8 @@
 
   def self_repository(): Repository = repository(Path.ISABELLE_HOME)
 
-  def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = {
-    @tailrec def find(root: Path): Option[Repository] =
-      detect_repository(root, ssh = ssh) match {
-        case None => if (root.is_root) None else find(root + Path.parent)
-        case some => some
-      }
-
-    find(ssh.expand_path(start))
-  }
+  def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
+    ssh.find_path(start, detect_repository(_, ssh = ssh))
 
   def the_repository(start: Path, ssh: SSH.System = SSH.Local): Repository =
     find_repository(start, ssh = ssh) getOrElse
diff -r 3956e8b6a9c9 -r e8d4ac2f21ea src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri May 24 16:15:27 2024 +0200
+++ b/src/Pure/General/ssh.scala	Fri May 24 17:06:57 2024 +0200
@@ -11,6 +11,8 @@
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
 
+import scala.annotation.tailrec
+
 
 object SSH {
   /* client command */
@@ -479,6 +481,16 @@
     def rsync_prefix: String = ""
     def rsync_path(path: Path): String = rsync_prefix + expand_path(path).implode
 
+    def find_path[A](start: Path, detect: Path => Option[A]): Option[A] = {
+      @tailrec def find(root: Path): Option[A] =
+        detect(root) match {
+          case None => if (root.is_root) None else find(root + Path.parent)
+          case some => some
+        }
+
+      find(expand_path(start))
+    }
+
     def expand_path(path: Path): Path = path.expand
     def absolute_path(path: Path): Path = path.absolute
     def bash_path(path: Path): String = File.bash_path(path)