tuned signature;
authorwenzelm
Mon, 08 May 2017 17:16:40 +0200
changeset 65778 666a1bac126b
parent 65777 821e77ce41be
child 65779 a42c9e375405
tuned signature;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
--- a/src/Pure/Admin/build_log.scala	Mon May 08 16:38:11 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon May 08 17:16:40 2017 +0200
@@ -703,7 +703,7 @@
       distinct: Boolean = false): SQL.Source =
     {
       val table2 = recent_pull_date_table(days)
-      table1.select(columns, distinct = distinct) + SQL.join_inner + table2.query_name +
+      table1.select(columns, distinct = distinct) + SQL.join_inner + table2.query_named +
       " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
     }
 
@@ -725,7 +725,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_name +
+          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_named +
           SQL.join_inner + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
         })
     }
--- a/src/Pure/General/sql.scala	Mon May 08 16:38:11 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 08 17:16:40 2017 +0200
@@ -133,7 +133,7 @@
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
-    def query_name: Source = query + " AS " + SQL.ident(name)
+    def query_named: Source = query + " AS " + SQL.ident(name)
 
     def create(strict: Boolean = false, sql_type: Type.Value => Source): Source =
     {