--- a/src/Pure/General/mercurial.scala Mon Nov 13 14:24:55 2017 +0100
+++ b/src/Pure/General/mercurial.scala Mon Nov 13 14:31:25 2017 +0100
@@ -52,23 +52,22 @@
find(ssh.expand_path(start))
}
- private def make_repository(root: Path, cmd: String, args: Repository => String,
- ssh: SSH.System = SSH.Local): Repository =
+ private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
+ : Repository =
{
val hg = new Repository(root, ssh)
ssh.mkdirs(hg.root.dir)
- hg.command(cmd, args(hg), repository = false).check
+ hg.command(cmd, args, repository = false).check
hg
}
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
- make_repository(root, "init", hg => File.bash_path(hg.root), ssh = ssh)
+ make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
def clone_repository(source: String, root: Path,
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "clone",
- hg => options + " " + Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev),
- ssh = ssh)
+ options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
{
@@ -90,7 +89,7 @@
{
val cmdline =
"\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
- (if (repository) " --repository " + File.bash_path(root) else "") +
+ (if (repository) " --repository " + ssh.bash_path(root) else "") +
" --noninteractive " + name + " " + options + " " + args
ssh.execute(cmdline)
}
--- a/src/Pure/General/ssh.scala Mon Nov 13 14:24:55 2017 +0100
+++ b/src/Pure/General/ssh.scala Mon Nov 13 14:31:25 2017 +0100
@@ -294,7 +294,7 @@
}
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
- def bash_path(path: Path): String = Bash.string(remote_path(path))
+ override def bash_path(path: Path): String = Bash.string(remote_path(path))
def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
@@ -400,6 +400,7 @@
def prefix: String = ""
def expand_path(path: Path): Path = path.expand
+ def bash_path(path: Path): String = File.bash_path(path)
def is_file(path: Path): Boolean = path.is_file
def is_dir(path: Path): Boolean = path.is_dir
def mkdirs(path: Path): Unit = Isabelle_System.mkdirs(path)