# HG changeset patch
# User wenzelm
# Date 1476557501 -7200
# Node ID 13a97c1d7d22f23d1ebeebed2096f95ac98fa252
# Parent  12aa3980f65c6d4ce1fe58d72cbcd8876f16d0ae
added setup_repository;
clarified root: expanded in target environment;

diff -r 12aa3980f65c -r 13a97c1d7d22 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Oct 15 20:47:31 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Oct 15 20:51:41 2016 +0200
@@ -32,18 +32,32 @@
   }
 
   def clone_repository(
-    source: String, dest: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
+    source: String, root: 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
+    val hg = new Repository(root, ssh)
+    hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
     hg
   }
 
-  class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session])
+  def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
+    ssh match {
+      case None => if (root.is_dir) repository(root) else clone_repository(source, root)
+      case Some(session) =>
+        using(session.sftp())(sftp =>
+          if (sftp.is_dir(sftp.path(root))) repository(root, ssh = ssh)
+          else clone_repository(source, root, ssh = ssh))
+    }
+
+  class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
   {
     hg =>
 
+    val root =
+      ssh match {
+        case None => root_path.expand
+        case Some(session) => using(session.sftp())(sftp => root_path.expand_env(sftp.settings))
+      }
+
     override def toString: String =
       ssh match {
         case None => root.implode
@@ -54,7 +68,7 @@
     {
       val cmdline =
         "\"${HG:-hg}\"" +
-          (if (name == "clone") "" else " --repository " + File.bash_string(root.implode)) +
+          (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
           " --noninteractive " + name + " " + options + " " + args
       ssh match {
         case None => Isabelle_System.bash(cmdline)