# HG changeset patch
# User wenzelm
# Date 1510579495 -3600
# Node ID d9a347af82ab977f65315dd05f17687008b62b2e
# Parent  fb487246ef4f016fec1861bb166d04dae18fafb4
more operations;

diff -r fb487246ef4f -r d9a347af82ab src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Nov 12 21:32:33 2017 +0100
+++ b/src/Pure/General/mercurial.scala	Mon Nov 13 14:24:55 2017 +0100
@@ -52,16 +52,24 @@
     find(ssh.expand_path(start))
   }
 
-  def clone_repository(source: String, root: Path, rev: String = "", options: String = "",
+  private def make_repository(root: Path, cmd: String, args: Repository => String,
     ssh: SSH.System = SSH.Local): Repository =
   {
     val hg = new Repository(root, ssh)
     ssh.mkdirs(hg.root.dir)
-    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root) + opt_rev(rev), options)
-      .check
+    hg.command(cmd, args(hg), 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)
+
+  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)
+
   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
   {
     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
@@ -77,11 +85,12 @@
 
     override def toString: String = ssh.prefix + root.implode
 
-    def command(name: String, args: String = "", options: String = ""): Process_Result =
+    def command(name: String, args: String = "", options: String = "",
+      repository: Boolean = true): Process_Result =
     {
       val cmdline =
         "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
-          (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
+          (if (repository) " --repository " + File.bash_path(root) else "") +
           " --noninteractive " + name + " " + options + " " + args
       ssh.execute(cmdline)
     }