clarified modules;
authorwenzelm
Wed, 29 Mar 2023 14:22:01 +0200
changeset 77744 1398add8c414
parent 77743 33bee7a96f72
child 77745 ebf70b199db7
clarified modules;
src/Pure/Admin/build_log.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/build_log.scala	Wed Mar 29 12:25:24 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Mar 29 14:22:01 2023 +0200
@@ -1114,4 +1114,19 @@
       Build_Info(sessions)
     }
   }
+
+
+  /* maintain build_log database */
+
+  def build_log_database(options: Options, log_dirs: List[Path],
+    snapshot: Option[Path] = None
+  ): Unit = {
+    val store = Build_Log.store(options)
+    using(store.open_database()) { db =>
+      db.vacuum()
+      store.update_database(db, log_dirs)
+      store.update_database(db, log_dirs, ml_statistics = true)
+      snapshot.foreach(store.snapshot_database(db, _))
+    }
+  }
 }
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 29 12:25:24 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 29 14:22:01 2023 +0200
@@ -596,7 +596,9 @@
                       (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
                     } yield remote_build_history(rev, afp_rev, i, r)))),
                 Logger_Task("build_log_database",
-                  logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
+                  logger =>
+                    Build_Log.build_log_database(logger.options, build_log_dirs,
+                      snapshot = Some(Isabelle_Devel.build_log_snapshot))),
                 Logger_Task("build_status",
                   logger => Isabelle_Devel.build_status(logger.options)))))),
             exit)))))
--- a/src/Pure/Admin/isabelle_devel.scala	Wed Mar 29 12:25:24 2023 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Wed Mar 29 14:22:01 2023 +0200
@@ -15,6 +15,7 @@
 
   val root: Path = Path.explode("~/html-data/devel")
   val cronjob_log: Path = root + Path.basic(CRONJOB_LOG)
+  val build_log_snapshot: Path = root + Path.explode(BUILD_LOG_DB)
 
 
   /* index */
@@ -49,19 +50,6 @@
   }
 
 
-  /* maintain build_log database */
-
-  def build_log_database(options: Options, log_dirs: List[Path]): Unit = {
-    val store = Build_Log.store(options)
-    using(store.open_database()) { db =>
-      db.vacuum()
-      store.update_database(db, log_dirs)
-      store.update_database(db, log_dirs, ml_statistics = true)
-      store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
-    }
-  }
-
-
   /* present build status */
 
   def build_status(options: Options): Unit = {