--- a/src/Pure/General/mercurial.scala Wed Oct 12 15:04:32 2016 +0200
+++ b/src/Pure/General/mercurial.scala Wed Oct 12 15:23:54 2016 +0200
@@ -24,38 +24,50 @@
/* repository access */
- def repository(root: Path): Repository = new Repository(root)
+ def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
+ new Repository(root, ssh)
- class Repository private[Mercurial](val root: Path)
+ class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session])
{
- override def toString: String = root.toString
+ hg =>
+
+ override def toString: String =
+ ssh match {
+ case None => root.implode
+ case Some(session) => quote(session.toString + ":" + root.implode)
+ }
- def command(cmd: String, cwd: JFile = null): Process_Result =
- Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd,
- cwd = cwd)
-
+ def command(cmd: String): Process_Result =
+ {
+ val cmdline =
+ "\"${HG:-hg}\" --repository " + File.bash_string(root.implode) + " --noninteractive " + cmd
+ ssh match {
+ case None => Isabelle_System.bash(cmdline)
+ case Some(session) => session.execute(cmdline)
+ }
+ }
def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
- command("heads " + options + opt_template(template)).check.out_lines
+ hg.command("heads " + options + opt_template(template)).check.out_lines
def identify(rev: String = "", options: String = ""): String =
- command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
+ hg.command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
def manifest(rev: String = "", options: String = ""): List[String] =
- command("manifest " + options + opt_rev(rev)).check.out_lines
+ hg.command("manifest " + options + opt_rev(rev)).check.out_lines
def log(rev: String = "", template: String = "", options: String = ""): String =
- command("log " + options + opt_rev(rev) + opt_template(template)).check.out
+ hg.command("log " + options + opt_rev(rev) + opt_template(template)).check.out
def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
- command("pull " + options + opt_rev(rev) + optional(remote)).check
+ hg.command("pull " + options + opt_rev(rev) + optional(remote)).check
def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
{
- command("update " + options +
+ hg.command("update " + options +
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check
}
- command("root").check
+ hg.command("root").check
}
}
--- a/src/Pure/System/isabelle_system.scala Wed Oct 12 15:04:32 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Oct 12 15:23:54 2016 +0200
@@ -317,9 +317,6 @@
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
- def hg(cmd_line: String, cwd: JFile = null): Process_Result =
- bash("\"${HG:-hg}\" " + cmd_line, cwd = cwd)
-
/** Isabelle resources **/