tuned: build hg_graph only once;
tuned signature;

--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 21 18:19:11 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Oct 22 13:12:38 2017 +0200
@@ -130,13 +130,6 @@
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, sql = sql)
 
-    def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
-    {
-      val rev0 = hg.id(history_base)
-      val nodes = hg.graph().all_succs(List(rev0)).toSet
-      (item: Item) => nodes(item.isabelle_version)
-    }
-
     def pick(
       options: Options,
       rev: String = "",
@@ -437,8 +430,16 @@
     File.write(main_state_file, main_start_date + " " + log_service.hostname)
 
     val hg = Mercurial.repository(isabelle_repos)
+    val hg_graph = hg.graph()
     val rev = hg.id()
 
+    def history_base_filter(r: Remote_Build): Item => Boolean =
+    {
+      val base_rev = hg.id(r.history_base)
+      val nodes = hg_graph.all_succs(List(base_rev)).toSet
+      (item: Item) => nodes(item.isabelle_version)
+    }
+
     run(main_start_date,
       Logger_Task("isabelle_cronjob", logger =>
         run_now(
@@ -447,7 +448,7 @@
               SEQ(
                 for {
                   (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
-                  (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, r.history_base_filter(hg))
+                  (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, history_base_filter(r))
                 } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
             Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
             Logger_Task("build_log_database",

--- a/src/Pure/General/mercurial.scala	Sat Oct 21 18:19:11 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Sun Oct 22 13:12:38 2017 +0200
@@ -16,6 +16,9 @@
 
 object Mercurial
 {
+  type Graph = isabelle.Graph[String, Unit]
+
+
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
@@ -119,7 +122,7 @@
     def known_files(): List[String] =
       hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
 
-    def graph(): Graph[String, Unit] =
+    def graph(): Graph =
     {
       val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
       val log_result =