clarified signature and modules: more explicit Build_Log.History;

--- a/src/Pure/Admin/build_log.scala	Sat Nov 18 21:14:34 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sun Nov 19 12:46:41 2023 +0100
@@ -1190,6 +1190,88 @@
   }
 
 
+
+  /** build history **/
+
+  object History {
+    sealed case class Entry(
+      known: Boolean,
+      isabelle_version: String,
+      afp_version: Option[String],
+      pull_date: Date
+    ) {
+      def unknown: Boolean = !known
+      def versions: (String, Option[String]) = (isabelle_version, afp_version)
+
+      def known_versions(rev: String, afp_rev: Option[String]): Boolean =
+        known && rev.nonEmpty && isabelle_version == rev &&
+        (afp_rev.isEmpty || afp_rev.get.nonEmpty && afp_version == afp_rev)
+    }
+
+    object Run {
+      val empty: Run = Run()
+      def longest(runs: List[Run]): Run = runs.foldLeft(empty)(_ max _)
+    }
+
+    sealed case class Run(entries: List[Entry] = Nil) {
+      def is_empty: Boolean = entries.isEmpty
+      val length: Int = entries.length
+      def max(other: Run): Run = if (length >= other.length) this else other
+      def median: Option[Entry] = if (is_empty) None else Some(entries(length / 2))
+
+      override def toString: String = {
+        val s = if (is_empty) "" else "length = " + length + ", median = " + median.get.pull_date
+        "Build_Log.History.Run(" + s + ")"
+      }
+    }
+
+    def retrieve(
+      db: SQL.Database,
+      days: Int,
+      rev: String,
+      afp_rev: Option[String],
+      sql: PostgreSQL.Source
+    ): History = {
+      val afp = afp_rev.isDefined
+
+      val entries =
+        db.execute_query_statement(
+          private_data.select_recent_versions(
+            days = days, rev = rev, afp_rev = afp_rev, sql = SQL.where(sql)),
+          List.from[Entry],
+          { res =>
+            val known = res.bool(private_data.known)
+            val isabelle_version = res.string(Prop.isabelle_version)
+            val afp_version = if (afp) proper_string(res.string(Prop.afp_version)) else None
+            val pull_date = res.date(private_data.pull_date(afp))
+            Entry(known, isabelle_version, afp_version, pull_date)
+          })
+
+      new History(entries)
+    }
+  }
+
+  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)
+      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
+        rest = b
+      }
+      result.toList
+    }
+  }
+
+
+
   /** maintain build_log database **/
 
   def build_log_database(options: Options, logs: List[Path],

--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 18 21:14:34 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 12:46:41 2023 +0100
@@ -118,53 +118,6 @@
 
   /* remote build_history */
 
-  sealed case class Item(
-    known: Boolean,
-    isabelle_version: String,
-    afp_version: Option[String],
-    pull_date: Date
-  ) {
-    def unknown: Boolean = !known
-    def versions: (String, Option[String]) = (isabelle_version, afp_version)
-
-    def known_versions(rev: String, afp_rev: Option[String]): Boolean =
-      known && rev.nonEmpty && isabelle_version == rev &&
-      (afp_rev.isEmpty || afp_rev.get.nonEmpty && afp_version == afp_rev)
-  }
-
-  def recent_items(
-    db: SQL.Database,
-    days: Int,
-    rev: String,
-    afp_rev: Option[String],
-    sql: PostgreSQL.Source
-  ): List[Item] = {
-    val afp = afp_rev.isDefined
-
-    db.execute_query_statement(
-      Build_Log.private_data.select_recent_versions(
-        days = days, rev = rev, afp_rev = afp_rev, sql = SQL.where(sql)),
-      List.from[Item],
-      { res =>
-        val known = res.bool(Build_Log.private_data.known)
-        val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
-        val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
-        val pull_date = res.date(Build_Log.private_data.pull_date(afp))
-        Item(known, isabelle_version, afp_version, pull_date)
-      })
-  }
-
-  def unknown_runs(items: List[Item]): List[List[Item]] = {
-    var rest = items
-    val result = new mutable.ListBuffer[List[Item]]
-    while (rest.nonEmpty) {
-      val (run, r) = Library.take_prefix[Item](_.unknown, rest.dropWhile(_.known))
-      if (run.nonEmpty) result += run
-      rest = r
-    }
-    result.toList
-  }
-
   sealed case class Remote_Build(
     description: String,
     host: String,
@@ -195,29 +148,26 @@
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
 
-    def pick(options: Options, filter: Item => Boolean): Option[(String, Option[String])] = {
+    def pick(
+      options: Options,
+      filter: Build_Log.History.Entry => Boolean
+    ): Option[(String, Option[String])] = {
       val rev = get_rev()
       val afp_rev = if (afp) Some(get_afp_rev()) else None
 
       val store = Build_Log.store(options)
       using(store.open_database()) { db =>
-        def pick_recent(days: Int, gap: Int): Option[(String, Option[String])] = {
-          val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
-          val runs = unknown_runs(items).filter(run => run.length >= gap)
-          val (longest_run, longest_length) =
-            runs.foldLeft((List.empty[Item], 0)) {
-              case (res@(item1, len1), item2) =>
-                val len2 = item2.length
-                if (len1 >= len2) res else (item2, len2)
-            }
-          if (longest_run.isEmpty) None
-          else Some(longest_run(longest_length / 2).versions)
+        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)
+          Build_Log.History.Run.longest(runs).median.map(_.versions)
         }
 
-        pick_recent(options.int("build_log_history") max history, 2) orElse
-        pick_recent(300, 8) orElse
-        pick_recent(3000, 32) orElse
-        pick_recent(0, 1)
+        get(options.int("build_log_history") max history, 2) orElse
+        get(300, 8) orElse
+        get(3000, 32) orElse
+        get(0, 1)
       }
     }
 
@@ -615,10 +565,10 @@
     val hg = Mercurial.repository(isabelle_repos)
     val hg_graph = hg.graph()
 
-    def history_base_filter(r: Remote_Build): Item => Boolean = {
+    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
-      (item: Item) => nodes(item.isabelle_version)
+      (entry: Build_Log.History.Entry) => nodes(entry.isabelle_version)
     }