--- a/src/Pure/Admin/build_log.scala Thu May 04 22:19:59 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Fri May 05 11:38:09 2017 +0200
@@ -700,7 +700,7 @@
{
val recent = recent_table(days)
val columns1 = if (pull_date) columns ::: List(Data.pull_date(recent)) else columns
- table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_alias() +
+ table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_name +
" ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
}
@@ -722,7 +722,7 @@
val columns = aux_columns ::: sessions_table.columns.tail
SQL.Table("isabelle_build_log", columns,
{
- SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_alias() +
+ SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_name +
" INNER JOIN " + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
})
}
--- a/src/Pure/General/sql.scala Thu May 04 22:19:59 2017 +0200
+++ b/src/Pure/General/sql.scala Fri May 05 11:38:09 2017 +0200
@@ -130,8 +130,7 @@
if (body == "") error("Missing SQL body for table " + quote(name))
else SQL.enclose(body)
- def query_alias(alias: String = name): String =
- query + " AS " + SQL.ident(alias)
+ def query_name: String = query + " AS " + SQL.ident(name)
def create(strict: Boolean = false, sql_type: Type.Value => String): String =
{