simplified: no internal state for Mercurial;

--- a/src/Pure/Admin/build_history.scala	Wed Oct 12 10:22:34 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Wed Oct 12 11:31:08 2016 +0200
@@ -370,19 +370,18 @@
           case _ => getopts.usage()
         }
 
-      using(Mercurial.open_repository(Path.explode(root)))(hg =>
-        {
-          val progress = new Console_Progress(stderr = true)
-          val results =
-            build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
-              components_base = components_base, fresh = fresh, nonfree = nonfree,
-              multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
-              heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
-              max_heap = max_heap, more_settings = more_settings, verbose = verbose,
-              build_args = build_args)
-          val rc = (0 /: results) { case (rc, res) => rc max res.rc }
-          if (rc != 0) sys.exit(rc)
-        })
+      val hg = Mercurial.repository(Path.explode(root))
+      val progress = new Console_Progress(stderr = true)
+      val results =
+        build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
+          components_base = components_base, fresh = fresh, nonfree = nonfree,
+          multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
+          heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
+          max_heap = max_heap, more_settings = more_settings, verbose = verbose,
+          build_args = build_args)
+
+      val rc = (0 /: results) { case (rc, res) => rc max res.rc }
+      if (rc != 0) sys.exit(rc)
     }
   }
 }

--- a/src/Pure/Admin/check_sources.scala	Wed Oct 12 10:22:34 2016 +0200
+++ b/src/Pure/Admin/check_sources.scala	Wed Oct 12 11:31:08 2016 +0200
@@ -44,12 +44,11 @@
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
-    using(Mercurial.open_repository(root)) { hg =>
-      for {
-        file <- hg.manifest()
-        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
-      } check_file(root + Path.explode(file))
-    }
+    val hg = Mercurial.repository(root)
+    for {
+      file <- hg.manifest()
+      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+    } check_file(root + Path.explode(file))
   }
 
 

--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Oct 12 10:22:34 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Oct 12 11:31:08 2016 +0200
@@ -25,12 +25,11 @@
   val afp_repos = main_dir + Path.explode("AFP-build_history")
 
   def pull_repos(root: Path): String =
-    using(Mercurial.open_repository(root))(hg =>
-      {
-        hg.pull(options = "-q")
-        hg.identify("tip", options = "-i")
-      })
-
+  {
+    val hg = Mercurial.repository(root)
+    hg.pull(options = "-q")
+    hg.identify("tip", options = "-i")
+  }
 
   /** cronjob **/
 

--- a/src/Pure/General/mercurial.scala	Wed Oct 12 10:22:34 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Oct 12 11:31:08 2016 +0200
@@ -24,14 +24,12 @@
 
   /* repository access */
 
-  def open_repository(root: Path): Repository = new Repository(root)
+  def repository(root: Path): Repository = new Repository(root)
 
   class Repository private[Mercurial](val root: Path)
   {
     override def toString: String = root.toString
 
-    def close() { }
-
     def command(cmd: String, cwd: JFile = null): Process_Result =
       Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd,
         cwd = cwd)