# HG changeset patch
# User wenzelm
# Date 1510579885 -3600
# Node ID 1645cef7a49c6019d0534974326f4e7bac400af8
# Parent  d9a347af82ab977f65315dd05f17687008b62b2e
proper ssh.bash_path;

diff -r d9a347af82ab -r 1645cef7a49c src/Pure/General/mercurial.scala
--- 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)
     }
diff -r d9a347af82ab -r 1645cef7a49c src/Pure/General/ssh.scala
--- 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)