# HG changeset patch
# User wenzelm
# Date 1493909386 -7200
# Node ID 681cdf83ce0946896131fa77fc76c5066aa9f599
# Parent  3ee466e890478e1cb39294eac0bd84c7dd2f8193
clarified universal view: include pull_date;

diff -r 3ee466e89047 -r 681cdf83ce09 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu May 04 15:38:24 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu May 04 16:49:46 2017 +0200
@@ -673,21 +673,6 @@
       build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
 
 
-    /* full view on build_log data */
-
-    val full_table: SQL.Table =
-    {
-      val columns = meta_info_table.columns ::: sessions_table.columns.tail
-      SQL.Table("isabelle_build_log", columns,
-        {
-          val table1 = meta_info_table
-          val table2 = sessions_table
-          SQL.select(log_name(table1) :: columns.tail) +
-          SQL.join(table1, table2, log_name(table1) + " = " + log_name(table2))
-        })
-    }
-
-
     /* earliest pull date for repository version (PostgreSQL queries) */
 
     val pull_date = SQL.Column.date("pull_date")
@@ -718,6 +703,29 @@
       table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_alias() +
       " ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
     }
+
+
+    /* universal view on main data */
+
+    val universal_table: SQL.Table =
+    {
+      val table1 = meta_info_table
+      val table2 = pull_date_table
+      val table3 = sessions_table
+
+      val aux_columns = log_name :: pull_date :: meta_info_table.columns.tail
+      val aux_table = SQL.Table("aux", aux_columns,
+        SQL.select(aux_columns.take(2) ::: aux_columns.drop(2). map(_.apply(table1))) +
+          table1 + " LEFT OUTER JOIN " + table2 + " ON " +
+          Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
+
+      val columns = aux_columns ::: sessions_table.columns.tail
+      SQL.Table("isabelle_build_log", columns,
+        {
+          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_alias() +
+          " INNER JOIN " + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
+        })
+    }
   }
 
 
@@ -749,8 +757,8 @@
     {
       write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
 
-      db.create_view(Data.full_table)
       db.create_view(Data.pull_date_table)
+      db.create_view(Data.universal_table)
     }
 
     def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
@@ -803,7 +811,7 @@
             }
 
             // full view
-            db2.create_view(Data.full_table)
+            db2.create_view(Data.universal_table)
           }
         }
         db2.rebuild