# HG changeset patch
# User wenzelm
# Date 1699115389 -3600
# Node ID 9f7a941176663d0ce6ca8eb095e18923d16bb032
# Parent  224aabe156f5c7d056577c32c352eea7eacdafa9
clarified "recent" time: days <= 0 means infinity (no constraint);

diff -r 224aabe156f5 -r 9f7a94117666 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 04 16:56:54 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 04 17:29:49 2023 +0100
@@ -720,11 +720,12 @@
 
     /* recent entries */
 
-    def recent_time(days: Int): PostgreSQL.Source =
-      "now() - INTERVAL '" + days.max(0) + " days'"
+    def recent(c: SQL.Column, days: Int): PostgreSQL.Source =
+      if (days <= 0) ""
+      else c.ident + " > now() - INTERVAL '" + days + " days'"
 
     def recent_pull_date_table(
-      days: Int,
+      days: Int = 0,
       rev: String = "",
       afp_rev: Option[String] = None
     ): SQL.Table = {
@@ -738,27 +739,27 @@
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns, sql =
           SQL.where_or(
-            pull_date(afp)(table).ident + " > " + recent_time(days),
+            recent(pull_date(afp)(table), days),
             SQL.and(eq_rev, eq_rev2))))
     }
 
-    def select_recent_log_names(days: Int): PostgreSQL.Source = {
+    def select_recent_log_names(days: Int = 0): PostgreSQL.Source = {
       val table1 = meta_info_table
-      val table2 = recent_pull_date_table(days)
+      val table2 = recent_pull_date_table(days = days)
       table1.select(List(log_name), distinct = true, sql =
         SQL.join_inner + table2.query_named +
         " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
     }
 
     def select_recent_versions(
-      days: Int,
+      days: Int = 0,
       rev: String = "",
       afp_rev: Option[String] = None,
       sql: PostgreSQL.Source = ""
     ): PostgreSQL.Source = {
       val afp = afp_rev.isDefined
       val version = Prop.isabelle_version
-      val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
+      val table1 = recent_pull_date_table(days = days, rev = rev, afp_rev = afp_rev)
       val table2 = meta_info_table
       val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
 
@@ -875,7 +876,7 @@
 
             val recent_log_names =
               db.execute_query_statement(
-                private_data.select_recent_log_names(days),
+                private_data.select_recent_log_names(days = days),
                 List.from[String], res => res.string(private_data.log_name))
 
             for (log_name <- recent_log_names) {
@@ -897,7 +898,7 @@
               db2.create_table(table)
               db2.using_statement(table.insert()) { stmt2 =>
                 db.using_statement(
-                  private_data.recent_pull_date_table(days, afp_rev = afp_rev).query) { stmt =>
+                  private_data.recent_pull_date_table(days = days, afp_rev = afp_rev).query) { stmt =>
                   using(stmt.execute_query()) { res =>
                     while (res.next()) {
                       for ((c, i) <- table.columns.zipWithIndex) {
diff -r 224aabe156f5 -r 9f7a94117666 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Nov 04 16:56:54 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Nov 04 17:29:49 2023 +0100
@@ -62,8 +62,7 @@
 
       Build_Log.private_data.universal_table.select(columns, distinct = true, sql =
         SQL.where_and(
-          Build_Log.private_data.pull_date(afp).ident + " > " +
-            Build_Log.private_data.recent_time(days(options)),
+          Build_Log.private_data.recent(Build_Log.private_data.pull_date(afp), days(options)),
           Build_Log.private_data.status.member(
             List(
               Build_Log.Session_Status.finished.toString,