# HG changeset patch
# User wenzelm
# Date 1475435114 -7200
# Node ID 5649a993666d9fcc3cec798fe324289109e5d5c6
# Parent  2f38d8aff2f5ff994ef59b4858ec4cea0dbc1184
more operations;

diff -r 2f38d8aff2f5 -r 5649a993666d src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun Oct 02 20:06:57 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Oct 02 21:05:14 2016 +0200
@@ -14,7 +14,12 @@
 {
   /* command-line syntax */
 
-  def opt_rev(rev: String): String = if (rev == "") "" else " --rev " + File.bash_string(rev)
+  def optional(s: String, prefix: String = ""): String =
+    if (s == "") "" else " " + prefix + " " + File.bash_string(s)
+
+  def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
+  def opt_rev(s: String): String = optional(s, "--rev")
+  def opt_template(s: String): String = optional(s, "--template")
 
 
   /* repository access */
@@ -30,12 +35,25 @@
     def command(cmd: String, cwd: JFile = null): Process_Result =
       Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd)
 
+
+    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
+      command("heads " + options + opt_template(template)).check.out_lines
+
     def identify(rev: String = "", options: String = ""): String =
       command("id -i " + 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
 
+    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
+      command("pull " + options + opt_rev(rev) + optional(remote)).check
+
+    def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
+    {
+      command("update " + options +
+        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check
+    }
+
     command("root").check
   }
 }