# HG changeset patch
# User wenzelm
# Date 1493904687 -7200
# Node ID 35fcedb6bdc8f81bd59b6a09a20370f209da6565
# Parent  01fc771021e67b64f283c0fc75da3e9791bf51c1
clarified database layout: pull date progression follows Isabelle only, and AFP is derived from that;

diff -r 01fc771021e6 -r 35fcedb6bdc8 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu May 04 15:20:57 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu May 04 15:31:27 2017 +0200
@@ -693,10 +693,10 @@
 
     val pull_date = SQL.Column.date("pull_date")
 
-    val isabelle_pull_date_table: SQL.Table =
+    val pull_date_table: SQL.Table =
     {
       val version = Prop.isabelle_version
-      build_log_table("isabelle_pull_date", List(version.copy(primary_key = true), pull_date),
+      build_log_table("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" +
@@ -705,7 +705,7 @@
 
     def recent_table(days: Int): SQL.Table =
     {
-      val table = isabelle_pull_date_table
+      val table = pull_date_table
       SQL.Table("recent", table.columns,
         table.select(table.columns) +
         " WHERE " + pull_date(table) + " > now() - INTERVAL '" + days.max(0) + " days'")
@@ -751,7 +751,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)
+        List(Data.full_table, Data.pull_date_table)
           .foreach(db.create_view(_))
       }
     }
@@ -789,7 +789,7 @@
 
             // pull_date
             {
-              val table = Data.isabelle_pull_date_table
+              val table = Data.pull_date_table
               db2.create_table(table)
               db2.using_statement(table.insert())(stmt2 =>
               {