--- 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
--- 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)