--- a/src/Pure/Admin/build_log.scala Mon May 01 17:28:25 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Mon May 01 20:14:50 2017 +0200
@@ -865,4 +865,26 @@
Build_Info(sessions)
}
}
+
+
+ /* full view on build_log data */
+
+ // WARNING: This may cause performance problems, e.g. with sqlitebrowser
+
+ val full_view: SQL.View =
+ SQL.View("isabelle_build_log",
+ Meta_Info.table.columns :::
+ Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)))
+
+ def create_full_view(db: SQL.Database)
+ {
+ if (!db.tables.contains(full_view.name)) {
+ val table1 = Meta_Info.table
+ val table2 = Build_Info.sessions_table
+ db.create_view(full_view,
+ SQL.select(Meta_Info.log_name(table1) :: full_view.columns.tail) +
+ SQL.join(table1, table2,
+ Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql))
+ }
+ }
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon May 01 17:28:25 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon May 01 20:14:50 2017 +0200
@@ -155,7 +155,15 @@
{
val store = Build_Log.store(options)
val files = Build_Log.Log_File.find_files(database_dirs)
- using(store.open_database())(db => store.write_info(db, files, ml_statistics = true))
+
+ // PostgreSQL server
+ using(store.open_database())(db =>
+ {
+ store.write_info(db, files, ml_statistics = true)
+ Build_Log.create_full_view(db)
+ })
+
+ // SQLite file
using(SQLite.open_database(build_log_snapshot))(db =>
{
store.write_info(db, files)