tuned signature;

--- a/src/Pure/Admin/build_log.scala	Wed May 03 14:55:34 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:10:22 2017 +0200
@@ -684,7 +684,7 @@
             val table1 = meta_info_table
             val table2 = sessions_table
             SQL.select(log_name(table1) :: columns.tail) +
-            SQL.join(table1, table2, log_name(table1).sql + " = " + log_name(table2).sql)
+            SQL.join(table1, table2, log_name(table1).ident + " = " + log_name(table2).ident)
           })
     }
 
@@ -696,22 +696,22 @@
     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.sql + ", min(" + Prop.build_start.sql + ") AS " + pull_date.sql +
-          " FROM " + meta_info_table.sql +
-          " WHERE " + version.sql + " IS NOT NULL AND" + Prop.build_start.sql + " IS NOT NULL" +
-          " GROUP BY " + version.sql)
+          "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)
 
     def recent(table: SQL.Table, days: Int): String =
       table.sql_select(table.columns) +
-      " WHERE " + pull_date(table).sql + " > now() - INTERVAL '" + days.max(0) + " days'"
+      " WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'"
 
     def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
       table.sql_select(columns) +
       " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
-      " ON " + Prop.isabelle_version(table).sql + " = recent." + Prop.isabelle_version.sql
+      " ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident
   }
 
 
@@ -927,12 +927,12 @@
 
       val where_log_name =
         Data.log_name(table1).sql_where_equal(log_name) + " AND " +
-          Data.session_name(table1).sql + " <> ''"
+          Data.session_name(table1).ident + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
         else
           where_log_name + " AND " +
-          session_names.map(a => Data.session_name(table1).sql + " = " + SQL.string(a)).
+          session_names.map(a => Data.session_name(table1).ident + " = " + SQL.string(a)).
             mkString("(", " OR ", ")")
 
       val columns1 = table1.columns.tail.map(_.apply(table1))
@@ -941,13 +941,13 @@
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
             SQL.join_outer(table1, table2,
-              Data.log_name(table1).sql + " = " +
-              Data.log_name(table2).sql + " AND " +
-              Data.session_name(table1).sql + " = " +
-              Data.session_name(table2).sql)
+              Data.log_name(table1).ident + " = " +
+              Data.log_name(table2).ident + " AND " +
+              Data.session_name(table1).ident + " = " +
+              Data.session_name(table2).ident)
           (columns, SQL.enclose(join))
         }
-        else (columns1, table1.sql)
+        else (columns1, table1.ident)
 
       val sessions =
         using(db.statement(SQL.select(columns) + from + " " + where))(stmt =>

--- a/src/Pure/General/sql.scala	Wed May 03 14:55:34 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 15:10:22 2017 +0200
@@ -33,17 +33,17 @@
   def string(s: String): String =
     "'" + s.map(escape_char(_)).mkString + "'"
 
-  def identifer(s: String): String =
+  def ident(s: String): String =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
 
   def enclose(s: String): String = "(" + s + ")"
   def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
 
   def select(columns: List[Column], distinct: Boolean = false): String =
-    "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.sql)) + " FROM "
+    "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " FROM "
 
   def join(table1: Table, table2: Table, sql: String = "", outer: Boolean = false): String =
-    table1.sql + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.sql +
+    table1.ident + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.ident +
       (if (sql == "") "" else " ON " + sql)
 
   def join_outer(table1: Table, table2: Table, sql: String = ""): String =
@@ -101,11 +101,12 @@
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
-    def sql: String = identifer(name)
+    def ident: String = SQL.ident(name)
+
     def sql_decl(sql_type: Type.Value => String): String =
-      identifer(name) + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
+      ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
-    def sql_where_eq: String = "WHERE " + identifer(name) + " = "
+    def sql_where_eq: String = "WHERE " + ident + " = "
     def sql_where_equal(s: String): String = sql_where_eq + string(s)
 
     override def toString: String = sql_decl(sql_type_default)
@@ -126,7 +127,7 @@
 
     def is_view: Boolean = view != ""
 
-    def sql: String = identifer(name)
+    def ident: String = SQL.ident(name)
 
     def sql_columns(sql_type: Type.Value => String): String =
     {
@@ -140,26 +141,24 @@
 
     def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        identifer(name) + " " + sql_columns(sql_type)
+        ident + " " + sql_columns(sql_type)
 
     def sql_create_index(
         index_name: String, index_columns: List[Column],
         strict: Boolean, unique: Boolean): String =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
-        (if (strict) "" else "IF NOT EXISTS ") + identifer(index_name) + " ON " +
-        identifer(name) + " " + enclosure(index_columns.map(_.name))
+        (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
+        ident + " " + enclosure(index_columns.map(_.name))
 
-    def sql_insert: String =
-      "INSERT INTO " + identifer(name) + " VALUES " + enclosure(columns.map(_ => "?"))
+    def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?"))
 
-    def sql_delete: String =
-      "DELETE FROM " + identifer(name)
+    def sql_delete: String = "DELETE FROM " + ident
 
     def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
-      select(select_columns, distinct = distinct) + identifer(name)
+      select(select_columns, distinct = distinct) + ident
 
     override def toString: String =
-      "TABLE " + identifer(name) + " " + sql_columns(sql_type_default)
+      "TABLE " + ident + " " + sql_columns(sql_type_default)
   }
 
 
@@ -308,7 +307,7 @@
     {
       require(table.is_view)
       if (strict || !tables.contains(table.name)) {
-        val sql = "CREATE VIEW " + identifer(table.name) + " AS " + table.view
+        val sql = "CREATE VIEW " + ident(table.name) + " AS " + table.view
         using(statement(sql))(_.execute())
       }
     }