clarified options;
authorwenzelm
Wed, 29 Mar 2023 21:23:56 +0200
changeset 77751 7ac59361791e
parent 77750 a8c52c99fa92
child 77752 1208ece65cca
clarified options;
src/Pure/Admin/build_log.scala
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/build_log.scala	Wed Mar 29 21:16:14 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Mar 29 21:23:56 2023 +0200
@@ -1150,6 +1150,7 @@
 
   def build_log_database(options: Options, log_dirs: List[Path],
     progress: Progress = new Progress,
+    vacuum: Boolean = false,
     ml_statistics: Boolean = false,
     snapshot: Option[Path] = None
   ): Unit = {
@@ -1161,7 +1162,7 @@
       ).sortBy(Log_File.plain_name)
 
     using(store.open_database()) { db =>
-      db.vacuum()
+      if (vacuum) db.vacuum()
 
       progress.echo("Updating database " + db + " ...")
       val errors0 = store.write_info(db, log_files, progress = progress)
@@ -1198,6 +1199,7 @@
     { args =>
       var ml_statistics: Boolean = false
       var snapshot: Option[Path] = None
+      var vacuum = false
       var dirs: List[Path] = Nil
       var options = Options.init()
       var verbose = false
@@ -1208,6 +1210,7 @@
   Options are:
     -M           include ML statistics
     -S FILE      snapshot to SQLite db file
+    -V           vacuum cleaning of database
     -d DIR       include directory with log files
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose
@@ -1217,6 +1220,7 @@
 """,
         "M" -> (_ => ml_statistics = true),
         "S:" -> (arg => snapshot = Some(Path.explode(arg))),
+        "V" -> (_ => vacuum = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "o:" -> (arg => options = options + arg),
         "v" -> (_ => verbose = true))
@@ -1226,7 +1230,7 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      build_log_database(options, dirs, progress = progress,
+      build_log_database(options, dirs, progress = progress, vacuum = vacuum,
         ml_statistics = ml_statistics, snapshot = snapshot)
     })
 }
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 29 21:16:14 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Mar 29 21:23:56 2023 +0200
@@ -598,7 +598,7 @@
                 Logger_Task("build_log_database",
                   logger =>
                     Build_Log.build_log_database(logger.options, build_log_dirs,
-                      ml_statistics = true,
+                      vacuum = true, ml_statistics = true,
                       snapshot = Some(Isabelle_Devel.build_log_snapshot))),
                 Logger_Task("build_status",
                   logger => Isabelle_Devel.build_status(logger.options)))))),