# HG changeset patch
# User wenzelm
# Date 1700419277 -3600
# Node ID 39fb869160d66982b2033e5b60e663fcd3fb3761
# Parent  674954a493642756c4698d7af109259a49ae94d9
clarified isabelle_hg (again, see b9d59669904a);

diff -r 674954a49364 -r 39fb869160d6 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 19:29:19 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 19:41:17 2023 +0100
@@ -23,11 +23,10 @@
   val build_log_database_log: Path = main_dir + Path.explode("run/build_log_database.log")
   val current_log: Path = main_dir + Path.explode("run/main.log")  // owned by log service
   val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
+  val isabelle_repos: Path = main_dir + Path.explode("isabelle")
+  val afp_repos: Path = main_dir + Path.explode("AFP")
 
-  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 isabelle_hg: Mercurial.Repository = Mercurial.self_repository()
   lazy val afp_hg: Mercurial.Repository = Mercurial.repository(afp_repos)
 
   val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
@@ -46,7 +45,7 @@
 
   /* init and exit */
 
-  def get_rev(hg: Mercurial.Repository = isabelle_hg): String = hg.id()
+  def get_rev(): String = isabelle_hg.id()
   def get_afp_rev(): String = afp_hg.id()
 
   val init: Logger_Task =
@@ -153,15 +152,11 @@
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
 
-    def history(
-      db: SQL.Database,
-      days: Int = 0,
-      hg: Mercurial.Repository = isabelle_hg
-    ): Build_Log.History = {
-      val rev = get_rev(hg = hg)
+    def history(db: SQL.Database, days: Int = 0): Build_Log.History = {
+      val rev = get_rev()
       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
+      val base_rev = isabelle_hg.id(history_base)
+      val filter_nodes = isabelle_hg.graph().all_succs(List(base_rev)).toSet
       Build_Log.History.retrieve(db, days, rev, afp_rev, sql,
         entry => filter_nodes(entry.isabelle_version))
     }