--- a/src/Pure/Admin/build_log.scala Tue May 02 21:42:03 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Tue May 02 21:57:32 2017 +0200
@@ -897,23 +897,17 @@
/* 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,
+ Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)),
+ {
+ val table1 = Meta_Info.table
+ val table2 = Build_Info.sessions_table
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))
- }
- }
+ Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql)
+ })
/* main operations */
@@ -923,7 +917,7 @@
{
val files = Log_File.find_files(dirs)
store.write_info(db, files, ml_statistics = ml_statistics)
- if (full_view) create_full_view(db)
+ if (full_view) db.create_view(Database.full_view)
}
}
}
--- a/src/Pure/General/sql.scala Tue May 02 21:42:03 2017 +0200
+++ b/src/Pure/General/sql.scala Tue May 02 21:57:32 2017 +0200
@@ -174,10 +174,11 @@
/* views */
- sealed case class View(name: String, columns: List[Column]) extends Qualifier
+ sealed case class View(name: String, columns: List[Column], query: String) extends Qualifier
{
def sql: String = identifer(name)
- def sql_create(query: String): String = "CREATE VIEW " + identifer(name) + " AS " + query
+ def sql_create: String = "CREATE VIEW " + identifer(name) + " AS " + query
+
override def toString: String =
"VIEW " + identifer(name) + " " + enclosure(columns.map(_.sql_decl(sql_type_default)))
}
@@ -329,8 +330,10 @@
def drop_index(table: Table, name: String, strict: Boolean = false): Unit =
using(statement(table.sql_drop_index(name, strict)))(_.execute())
- def create_view(view: View, query: String): Unit =
- using(statement(view.sql_create(query)))(_.execute())
+ def create_view(view: View, strict: Boolean = false): Unit =
+ if (strict || !tables.contains(view.name)) {
+ using(statement(view.sql_create))(_.execute())
+ }
}
}