tuned signature;

--- a/src/Pure/Admin/build_log.scala	Wed May 03 15:10:22 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:16:55 2017 +0200
@@ -679,13 +679,12 @@
         meta_info_table.columns :::
           sessions_table.columns.tail.map(_.copy(primary_key = false))
       SQL.Table("isabelle_build_log", columns,
-        view =
-          {
-            val table1 = meta_info_table
-            val table2 = sessions_table
-            SQL.select(log_name(table1) :: columns.tail) +
-            SQL.join(table1, table2, log_name(table1).ident + " = " + log_name(table2).ident)
-          })
+        {
+          val table1 = meta_info_table
+          val table2 = sessions_table
+          SQL.select(log_name(table1) :: columns.tail) +
+          SQL.join(table1, table2, log_name(table1).ident + " = " + log_name(table2).ident)
+        })
     }
 
 
@@ -695,11 +694,11 @@
 
     def pull_date_table(name: String, version: SQL.Column): SQL.Table =
       SQL.Table("isabelle_build_log_" + name, List(version.copy(primary_key = true), pull_date),
-        view = // PostgreSQL
-          "SELECT " + version.ident + ", min(" + Prop.build_start.ident + ") AS " + pull_date.ident +
-          " FROM " + meta_info_table.ident +
-          " WHERE " + version.ident + " IS NOT NULL AND" + Prop.build_start.ident + " IS NOT NULL" +
-          " GROUP BY " + version.ident)
+        // PostgreSQL
+        "SELECT " + version.ident + ", min(" + Prop.build_start.ident + ") AS " + pull_date.ident +
+        " FROM " + meta_info_table.ident +
+        " WHERE " + version.ident + " IS NOT NULL AND" + Prop.build_start.ident + " IS NOT NULL" +
+        " GROUP BY " + version.ident)
 
     val isabelle_pull_date_table = pull_date_table("isabelle_pull_date", Prop.isabelle_version)
     val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)

--- a/src/Pure/General/sql.scala	Wed May 03 15:10:22 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 15:16:55 2017 +0200
@@ -115,7 +115,7 @@
 
   /* tables */
 
-  sealed case class Table(name: String, columns: List[Column], view: String = "")
+  sealed case class Table(name: String, columns: List[Column], body: String = "")
   {
     private val columns_index: Map[String, Int] =
       columns.iterator.map(_.name).zipWithIndex.toMap
@@ -125,9 +125,11 @@
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
-    def is_view: Boolean = view != ""
+    def ident: String = SQL.ident(name)
 
-    def ident: String = SQL.ident(name)
+    def expr: String =
+      if (body == "") error("Missing SQL body for table " + quote(name))
+      else SQL.enclose(body)
 
     def sql_columns(sql_type: Type.Value => String): String =
     {
@@ -305,9 +307,8 @@
 
     def create_view(table: Table, strict: Boolean = false): Unit =
     {
-      require(table.is_view)
       if (strict || !tables.contains(table.name)) {
-        val sql = "CREATE VIEW " + ident(table.name) + " AS " + table.view
+        val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
         using(statement(sql))(_.execute())
       }
     }