# HG changeset patch
# User wenzelm
# Date 1493888808 -7200
# Node ID 1626b73daccf039faa70e795567ef693d0cba014
# Parent  50a61990c01e8c539664681e6a1ad49beeeb5332
eliminated unused afp_pull_date table;
tuned;

diff -r 50a61990c01e -r 1626b73daccf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu May 04 00:19:05 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu May 04 11:06:48 2017 +0200
@@ -695,19 +695,20 @@
 
     val pull_date = SQL.Column.date("pull_date")
 
-    def pull_date_table(name: String, version: SQL.Column): SQL.Table =
-      build_log_table(name, List(version.copy(primary_key = true), pull_date),
+    val isabelle_pull_date_table: SQL.Table =
+    {
+      val version = Prop.isabelle_version
+      build_log_table("isabelle_pull_date", List(version.copy(primary_key = true), pull_date),
         "SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
         " FROM " + meta_info_table +
         " WHERE " + version + " IS NOT NULL AND " + Prop.build_start + " IS NOT NULL" +
         " GROUP BY " + version)
-
-    val isabelle_pull_date_table = pull_date_table("isabelle_pull_date", Prop.isabelle_version)
-    val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)
+    }
 
-    def recent_table(table: SQL.Table, days: Int, alias: String = ""): SQL.Table =
+    def recent_table(days: Int): SQL.Table =
     {
-      SQL.Table(if (alias == "") table.name else alias, table.columns,
+      val table = isabelle_pull_date_table
+      SQL.Table("recent", table.columns,
         table.select(table.columns) +
         " WHERE " + pull_date(table) + " > now() - INTERVAL '" + days.max(0) + " days'")
     }
@@ -715,7 +716,7 @@
     def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int,
       distinct: Boolean = false, pull_date: Boolean = false): String =
     {
-      val recent = recent_table(isabelle_pull_date_table, days, "recent")
+      val recent = recent_table(days)
       val columns1 = if (pull_date) columns ::: List(Data.pull_date(recent)) else columns
       table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_alias() +
       " ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
@@ -752,7 +753,7 @@
       write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
 
       if (db.isInstanceOf[PostgreSQL.Database]) {
-        List(Data.full_table, Data.isabelle_pull_date_table, Data.afp_pull_date_table)
+        List(Data.full_table, Data.isabelle_pull_date_table)
           .foreach(db.create_view(_))
       }
     }
@@ -789,12 +790,12 @@
             }
 
             // pull_date
-            List(Data.isabelle_pull_date_table, Data.afp_pull_date_table).foreach(table =>
             {
+              val table = Data.isabelle_pull_date_table
               db2.create_table(table)
               db2.using_statement(table.insert())(stmt2 =>
               {
-                db.using_statement(Data.recent_table(table, days).query)(stmt =>
+                db.using_statement(Data.recent_table(days).query)(stmt =>
                 {
                   val rs = stmt.executeQuery
                   while (rs.next()) {
@@ -804,7 +805,7 @@
                   }
                 })
               })
-            })
+            }
 
             // full view
             db2.create_view(Data.full_table)