# HG changeset patch
# User wenzelm
# Date 1493755052 -7200
# Node ID 74ec3cfcb6bfdc46cfd05691d78eea5409e6b89d
# Parent  c1eab527bfa7cf667efa47f54645ea4dacc93443
tuned;

diff -r c1eab527bfa7 -r 74ec3cfcb6bf src/Pure/Admin/build_log.scala
--- 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)
     }
   }
 }
diff -r c1eab527bfa7 -r 74ec3cfcb6bf src/Pure/General/sql.scala
--- 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())
+      }
   }
 }