src/Pure/General/mercurial.scala
changeset 67066 1645cef7a49c
parent 67065 d9a347af82ab
child 67068 46ce32fd5f53
equal deleted inserted replaced
67065:d9a347af82ab 67066:1645cef7a49c
    50       else find(root + Path.parent)
    50       else find(root + Path.parent)
    51 
    51 
    52     find(ssh.expand_path(start))
    52     find(ssh.expand_path(start))
    53   }
    53   }
    54 
    54 
    55   private def make_repository(root: Path, cmd: String, args: Repository => String,
    55   private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
    56     ssh: SSH.System = SSH.Local): Repository =
    56     : Repository =
    57   {
    57   {
    58     val hg = new Repository(root, ssh)
    58     val hg = new Repository(root, ssh)
    59     ssh.mkdirs(hg.root.dir)
    59     ssh.mkdirs(hg.root.dir)
    60     hg.command(cmd, args(hg), repository = false).check
    60     hg.command(cmd, args, repository = false).check
    61     hg
    61     hg
    62   }
    62   }
    63 
    63 
    64   def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
    64   def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
    65     make_repository(root, "init", hg => File.bash_path(hg.root), ssh = ssh)
    65     make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
    66 
    66 
    67   def clone_repository(source: String, root: Path,
    67   def clone_repository(source: String, root: Path,
    68       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
    68       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
    69     make_repository(root, "clone",
    69     make_repository(root, "clone",
    70       hg => options + " " + Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev),
    70       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
    71       ssh = ssh)
       
    72 
    71 
    73   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
    72   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
    74   {
    73   {
    75     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    74     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    76     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
    75     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
    88     def command(name: String, args: String = "", options: String = "",
    87     def command(name: String, args: String = "", options: String = "",
    89       repository: Boolean = true): Process_Result =
    88       repository: Boolean = true): Process_Result =
    90     {
    89     {
    91       val cmdline =
    90       val cmdline =
    92         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
    91         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
    93           (if (repository) " --repository " + File.bash_path(root) else "") +
    92           (if (repository) " --repository " + ssh.bash_path(root) else "") +
    94           " --noninteractive " + name + " " + options + " " + args
    93           " --noninteractive " + name + " " + options + " " + args
    95       ssh.execute(cmdline)
    94       ssh.execute(cmdline)
    96     }
    95     }
    97 
    96 
    98     def archive(target: String, rev: String = "", options: String = ""): Unit =
    97     def archive(target: String, rev: String = "", options: String = ""): Unit =