--- 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())
}
}