# HG changeset patch
# User wenzelm
# Date 1700403309 -3600
# Node ID b9d59669904a975c2656ab7d1e210491230cf21e
# Parent  07f135271c8044be6c5ad6784a2af94a8fc41bc4
clarified signature: more operations and options concerning Isabelle hg;

diff -r 07f135271c80 -r b9d59669904a src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Nov 19 14:48:11 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Nov 19 15:15:09 2023 +0100
@@ -1226,7 +1226,8 @@
       days: Int,
       rev: String,
       afp_rev: Option[String],
-      sql: PostgreSQL.Source
+      sql: PostgreSQL.Source,
+      filter: Entry => Boolean = _ => true
     ): History = {
       val afp = afp_rev.isDefined
 
@@ -1243,23 +1244,20 @@
             Entry(known, isabelle_version, afp_version, pull_date)
           })
 
-      new History(entries)
+      new History(entries.filter(filter))
     }
   }
 
   final class History private(val entries: List[History.Entry]) {
     override def toString: String = "Build_Log.History(" + entries.length + ")"
 
-    def unknown_runs(
-      pre: History.Entry => Boolean = _ => true,
-      post: History.Run => Boolean = _ => true
-    ): List[History.Run] = {
-      var rest = entries.filter(pre)
+    def unknown_runs(filter: History.Run => Boolean = _ => true): List[History.Run] = {
+      var rest = entries
       val result = new mutable.ListBuffer[History.Run]
       while (rest.nonEmpty) {
         val (a, b) = Library.take_prefix[History.Entry](_.unknown, rest.dropWhile(_.known))
         val run = History.Run(a)
-        if (!run.is_empty && post(run)) result += run
+        if (!run.is_empty && filter(run)) result += run
         rest = b
       }
       result.toList
diff -r 07f135271c80 -r b9d59669904a src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 14:48:11 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 15:15:09 2023 +0100
@@ -25,7 +25,10 @@
   val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
 
   val isabelle_repos: Path = main_dir + Path.explode("isabelle")
+  lazy val isabelle_hg: Mercurial.Repository = Mercurial.repository(isabelle_repos)
+
   val afp_repos: Path = main_dir + Path.explode("AFP")
+  lazy val afp_hg: Mercurial.Repository = Mercurial.repository(afp_repos)
 
   val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
 
@@ -43,8 +46,8 @@
 
   /* init and exit */
 
-  def get_rev(): String = Mercurial.repository(isabelle_repos).id()
-  def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
+  def get_rev(hg: Mercurial.Repository = isabelle_hg): String = hg.id()
+  def get_afp_rev(): String = afp_hg.id()
 
   val init: Logger_Task =
     Logger_Task("init",
@@ -148,19 +151,25 @@
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
 
-    def pick(
-      options: Options,
-      filter: Build_Log.History.Entry => Boolean
-    ): Option[(String, Option[String])] = {
-      val rev = get_rev()
+    def history(
+      db: SQL.Database,
+      days: Int = 0,
+      hg: Mercurial.Repository = isabelle_hg
+    ): Build_Log.History = {
+      val rev = get_rev(hg = hg)
       val afp_rev = if (afp) Some(get_afp_rev()) else None
+      val base_rev = hg.id(history_base)
+      val filter_nodes = hg.graph().all_succs(List(base_rev)).toSet
+      Build_Log.History.retrieve(db, days, rev, afp_rev, sql,
+        entry => filter_nodes(entry.isabelle_version))
+    }
+
+    def pick(options: Options): Option[(String, Option[String])] = {
 
       val store = Build_Log.store(options)
       using(store.open_database()) { db =>
         def get(days: Int, gap: Int): Option[(String, Option[String])] = {
-          val runs =
-            Build_Log.History.retrieve(db, days, rev, afp_rev, sql)
-              .unknown_runs(pre = filter, post = run => run.length >= gap)
+          val runs = history(db, days = days).unknown_runs(filter = run => run.length >= gap)
           Build_Log.History.Run.longest(runs).median.map(_.versions)
         }
 
@@ -560,18 +569,6 @@
         })
 
 
-    /* repository structure */
-
-    val hg = Mercurial.repository(isabelle_repos)
-    val hg_graph = hg.graph()
-
-    def history_base_filter(r: Remote_Build): Build_Log.History.Entry => Boolean = {
-      val base_rev = hg.id(r.history_base)
-      val nodes = hg_graph.all_succs(List(base_rev)).toSet
-      (entry: Build_Log.History.Entry) => nodes(entry.isabelle_version)
-    }
-
-
     /* main */
 
     val main_start_date = Date.now()
@@ -604,7 +601,7 @@
                       for {
                         (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
                       } yield () => {
-                        r.pick(logger.options, history_base_filter(r))
+                        r.pick(logger.options)
                           .map({ case (rev, afp_rev) =>
                             remote_build_history(rev, afp_rev, i, r,
                               progress = build_log_database_progress) })