# HG changeset patch
# User wenzelm
# Date 1476280085 -7200
# Node ID e573b985390c082380c242a786891135f1f2f5d5
# Parent  097d122222f620f98549f7993eb8ad422e02dbcb
added clone_repository;
tuned;

diff -r 097d122222f6 -r e573b985390c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Oct 12 15:23:54 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Oct 12 15:48:05 2016 +0200
@@ -25,7 +25,20 @@
   /* repository access */
 
   def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
-    new Repository(root, ssh)
+  {
+    val hg = new Repository(root, ssh)
+    hg.command("root").check
+    hg
+  }
+
+  def clone_repository(
+    source: String, dest: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
+  {
+    val hg = new Repository(dest, ssh)
+    hg.command("clone",
+      File.bash_string(source) + " " + File.bash_string(dest.implode), options).check
+    hg
+  }
 
   class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session])
   {
@@ -37,10 +50,12 @@
         case Some(session) => quote(session.toString + ":" + root.implode)
       }
 
-    def command(cmd: String): Process_Result =
+    def command(name: String, args: String = "", options: String = ""): Process_Result =
     {
       val cmdline =
-        "\"${HG:-hg}\" --repository " + File.bash_string(root.implode) + " --noninteractive " + cmd
+        "\"${HG:-hg}\"" +
+          (if (name == "clone") "" else " --repository " + File.bash_string(root.implode)) +
+          " --noninteractive " + name + " " + options + " " + args
       ssh match {
         case None => Isabelle_System.bash(cmdline)
         case Some(session) => session.execute(cmdline)
@@ -48,26 +63,25 @@
     }
 
     def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
-      hg.command("heads " + options + opt_template(template)).check.out_lines
+      hg.command("heads", opt_template(template), options).check.out_lines
 
     def identify(rev: String = "", options: String = ""): String =
-      hg.command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
+      hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
 
     def manifest(rev: String = "", options: String = ""): List[String] =
-      hg.command("manifest " + options + opt_rev(rev)).check.out_lines
+      hg.command("manifest", opt_rev(rev), options).check.out_lines
 
     def log(rev: String = "", template: String = "", options: String = ""): String =
-      hg.command("log " + options + opt_rev(rev) + opt_template(template)).check.out
+      hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
 
     def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
-      hg.command("pull " + options + opt_rev(rev) + optional(remote)).check
+      hg.command("pull", opt_rev(rev) + optional(remote), options).check
 
-    def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
+    def update(
+      rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
     {
-      hg.command("update " + options +
-        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check
+      hg.command("update",
+        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
     }
-
-    hg.command("root").check
   }
 }