# HG changeset patch
# User wenzelm
# Date 1493566632 -7200
# Node ID 0818da4f67bb6234c8c5aa38bc17e72a4c2dbadc
# Parent  69dfec14b0dff4e889aa62641df1cd01e31a2cb7
tuned signature;

diff -r 69dfec14b0df -r 0818da4f67bb src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sun Apr 30 17:32:14 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sun Apr 30 17:37:12 2017 +0200
@@ -807,12 +807,12 @@
 
       val where_log_name =
         Meta_Info.log_name(table1).sql_where_equal(log_name) + " AND " +
-          Build_Info.session_name(table1).sql_name + " <> ''"
+          Build_Info.session_name(table1).sql + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
         else
           where_log_name + " AND " +
-          session_names.map(a => Build_Info.session_name(table1).sql_name + " = " + SQL.string(a)).
+          session_names.map(a => Build_Info.session_name(table1).sql + " = " + SQL.string(a)).
             mkString("(", " OR ", ")")
 
       val columns1 = table1.columns.tail.map(_.apply(table1))
@@ -820,17 +820,14 @@
         if (ml_statistics) {
           val columns = columns1 ::: List(Build_Info.ml_statistics(table2))
           val from =
-            "(" +
-              SQL.ident(table1.name) + " LEFT JOIN " +
-              SQL.ident(table2.name) + " ON " +
-              Meta_Info.log_name(table1).sql_name + " = " +
-              Meta_Info.log_name(table2).sql_name + " AND " +
-              Build_Info.session_name(table1).sql_name + " = " +
-              Build_Info.session_name(table2).sql_name +
-            ")"
+            "(" + table1.sql + " LEFT JOIN " + table2.sql + " ON " +
+              Meta_Info.log_name(table1).sql + " = " +
+              Meta_Info.log_name(table2).sql + " AND " +
+              Build_Info.session_name(table1).sql + " = " +
+              Build_Info.session_name(table2).sql + ")"
           (columns, from)
         }
-        else (columns1, SQL.ident(table1.name))
+        else (columns1, table1.sql)
 
       val sessions =
         using(db.statement(SQL.select(columns) + from + " " + where))(stmt =>
diff -r 69dfec14b0df -r 0818da4f67bb src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Apr 30 17:32:14 2017 +0200
+++ b/src/Pure/General/sql.scala	Sun Apr 30 17:37:12 2017 +0200
@@ -40,7 +40,7 @@
   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_name)) + " FROM "
+    "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.sql)) + " FROM "
 
 
   /* types */
@@ -94,11 +94,11 @@
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
-    def sql_name: String = ident(name)
+    def sql: String = ident(name)
     def sql_decl(sql_type: Type.Value => String): String =
-      sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
+      sql + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
-    def sql_where_eq: String = "WHERE " + sql_name + " = "
+    def sql_where_eq: String = "WHERE " + sql + " = "
     def sql_where_equal(s: String): String = sql_where_eq + string(s)
 
     override def toString: String = sql_decl(sql_type_default)
@@ -117,6 +117,8 @@
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
+    def sql: String = ident(name)
+
     def sql_columns(sql_type: Type.Value => String): String =
     {
       val primary_key =