more operations;
authorwenzelm
Mon Nov 13 14:24:55 2017 +0100 (9 months ago)
changeset 67065d9a347af82ab
parent 67064 fb487246ef4f
child 67066 1645cef7a49c
more operations;
src/Pure/General/mercurial.scala
     1.1 --- a/src/Pure/General/mercurial.scala	Sun Nov 12 21:32:33 2017 +0100
     1.2 +++ b/src/Pure/General/mercurial.scala	Mon Nov 13 14:24:55 2017 +0100
     1.3 @@ -52,16 +52,24 @@
     1.4      find(ssh.expand_path(start))
     1.5    }
     1.6  
     1.7 -  def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
     1.8 +  private def make_repository(root: Path, cmd: String, args: Repository => String,
     1.9      ssh: SSH.System = SSH.Local): Repository =
    1.10    {
    1.11      val hg = new Repository(root, ssh)
    1.12      ssh.mkdirs(hg.root.dir)
    1.13 -    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
    1.14 -      .check
    1.15 +    hg.command(cmd, args(hg), repository = false).check
    1.16      hg
    1.17    }
    1.18  
    1.19 +  def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
    1.20 +    make_repository(root, "init", hg => File.bash_path(hg.root), ssh = ssh)
    1.21 +
    1.22 +  def clone_repository(source: String, root: Path,
    1.23 +      rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
    1.24 +    make_repository(root, "clone",
    1.25 +      hg => options + " " + Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev),
    1.26 +      ssh = ssh)
    1.27 +
    1.28    def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
    1.29    {
    1.30      if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
    1.31 @@ -77,11 +85,12 @@
    1.32  
    1.33      override def toString: String = ssh.prefix + root.implode
    1.34  
    1.35 -    def command(name: String, args: String = "", options: String = ""): Process_Result =
    1.36 +    def command(name: String, args: String = "", options: String = "",
    1.37 +      repository: Boolean = true): Process_Result =
    1.38      {
    1.39        val cmdline =
    1.40          "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
    1.41 -          (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
    1.42 +          (if (repository) " --repository " + File.bash_path(root) else "") +
    1.43            " --noninteractive " + name + " " + options + " " + args
    1.44        ssh.execute(cmdline)
    1.45      }