# HG changeset patch
# User wenzelm
# Date 1507924402 -7200
# Node ID 2ca6f0275de734bd1023c4c0366ccb45caeb1d95
# Parent  f8f42289c4dfc9266501173bbc7ca89556073a24
support for AFP versions;

diff -r f8f42289c4df -r 2ca6f0275de7 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Oct 13 21:20:31 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Oct 13 21:53:22 2017 +0200
@@ -727,9 +727,9 @@
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
-    def recent_pull_date_table(days: Int, rev: String = ""): SQL.Table =
+    def recent_pull_date_table(days: Int, rev: String = "", afp: Boolean = false): SQL.Table =
     {
-      val table = pull_date_table
+      val table = if (afp) afp_pull_date_table else pull_date_table
       SQL.Table("recent_pull_date", table.columns,
         table.select(table.columns,
           "WHERE " + pull_date(table) + " > " + recent_time(days) +
@@ -744,19 +744,20 @@
         " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
     }
 
-    def select_recent_isabelle_versions(days: Int, rev: String = "", sql: SQL.Source = "")
-      : SQL.Source =
+    def select_recent_versions(
+      days: Int, rev: String = "", afp: Boolean = false, sql: SQL.Source = ""): SQL.Source =
     {
-      val table1 = recent_pull_date_table(days, rev = rev)
+      val version = Prop.isabelle_version
+      val table1 = recent_pull_date_table(days, rev = rev, afp = afp)
       val table2 = meta_info_table
       val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
 
       val columns =
-        List(Prop.isabelle_version(table1), pull_date(table1),
-          known.copy(expr = log_name(aux_table).defined))
+        table1.columns.map(c => c(table1)) :::
+          List(known.copy(expr = log_name(aux_table).defined))
       SQL.select(columns, distinct = true) +
         table1.query_named + SQL.join_outer + aux_table.query_named +
-        " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(aux_table) +
+        " ON " + version(table1) + " = " + version(aux_table) +
         " ORDER BY " + pull_date(table1) + " DESC"
     }
 
diff -r f8f42289c4df -r 2ca6f0275de7 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Oct 13 21:20:31 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Oct 13 21:53:22 2017 +0200
@@ -77,7 +77,7 @@
   def recent_items(db: SQL.Database, days: Int, rev: String, sql: SQL.Source): List[Item] =
   {
     val select =
-      Build_Log.Data.select_recent_isabelle_versions(days = days, rev = rev, sql = "WHERE " + sql)
+      Build_Log.Data.select_recent_versions(days = days, rev = rev, sql = "WHERE " + sql)
 
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>