# HG changeset patch
# User wenzelm
# Date 1507921775 -7200
# Node ID c9d413fca1ece26f92302df4773a6b00e75794f2
# Parent  e23d73f43fb6079119a8fde19720ac0ef63f430c
support for AFP versions;

diff -r e23d73f43fb6 -r c9d413fca1ec src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Oct 13 13:31:56 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Oct 13 21:09:35 2017 +0200
@@ -684,6 +684,18 @@
       build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
 
 
+    /* AFP versions */
+
+    val isabelle_afp_versions_table: SQL.Table =
+    {
+      val version1 = Prop.isabelle_version
+      val version2 = Prop.afp_version
+      build_log_table("isabelle_afp_versions", List(version1.copy(primary_key = true), version2),
+        SQL.select(List(version1, version2), distinct = true) + meta_info_table +
+        " WHERE " + version1 + " IS NOT NULL AND " + version2 + " IS NOT NULL")
+    }
+
+
     /* earliest pull date for repository version (PostgreSQL queries) */
 
     val pull_date = SQL.Column.date("pull_date")
@@ -698,6 +710,20 @@
         " GROUP BY " + version)
     }
 
+    val afp_pull_date_table: SQL.Table =
+    {
+      val version1 = Prop.isabelle_version
+      val version2 = Prop.afp_version
+      val table1 = pull_date_table
+      val table2 = isabelle_afp_versions_table
+      build_log_table("afp_pull_date", List(version1.copy(primary_key = true), version2, pull_date),
+        table1.select(List(version1(table1), version2(table2), pull_date(table1))) +
+        SQL.join_inner + table2.query_named + " ON " + version1(table1) + " = " + version1(table2))
+    }
+
+
+    /* recent entries */
+
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
@@ -799,6 +825,7 @@
       write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
 
       db.create_view(Data.pull_date_table)
+      db.create_view(Data.afp_pull_date_table)
       db.create_view(Data.universal_table)
     }