# HG changeset patch
# User wenzelm
# Date 1493820909 -7200
# Node ID d788c11176e59edf05cc4f773b46af2ac188a7d3
# Parent  333961e15062fdb7393ee1ba72ce96b25f2bc6a8
simplified: standard toString is SQL.ident;

diff -r 333961e15062 -r d788c11176e5 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 03 16:01:01 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 16:15:09 2017 +0200
@@ -686,7 +686,7 @@
           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)
+          SQL.join(table1, table2, log_name(table1) + " = " + log_name(table2))
         })
     }
 
@@ -698,22 +698,22 @@
     def pull_date_table(name: String, version: SQL.Column): SQL.Table =
       table(name, List(version.copy(primary_key = true), pull_date),
         // 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)
+        "SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
+        " FROM " + meta_info_table +
+        " WHERE " + version + " IS NOT NULL AND " + Prop.build_start + " IS NOT NULL" +
+        " GROUP BY " + version)
 
     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.select(table.columns) +
-      " WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'"
+      " WHERE " + pull_date(table) + " > now() - INTERVAL '" + days.max(0) + " days'"
 
     def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
       table.select(columns) +
       " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
-      " ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident
+      " ON " + Prop.isabelle_version(table) + " = recent." + Prop.isabelle_version
   }
 
 
@@ -929,12 +929,12 @@
 
       val where_log_name =
         Data.log_name(table1).where_equal(log_name) + " AND " +
-          Data.session_name(table1).ident + " <> ''"
+        Data.session_name(table1) + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
         else
           where_log_name + " AND " +
-          session_names.map(a => Data.session_name(table1).ident + " = " + SQL.string(a)).
+          session_names.map(a => Data.session_name(table1) + " = " + SQL.string(a)).
             mkString("(", " OR ", ")")
 
       val columns1 = table1.columns.tail.map(_.apply(table1))
@@ -943,10 +943,8 @@
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
             SQL.join_outer(table1, table2,
-              Data.log_name(table1).ident + " = " +
-              Data.log_name(table2).ident + " AND " +
-              Data.session_name(table1).ident + " = " +
-              Data.session_name(table2).ident)
+              Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
+              Data.session_name(table1) + " = " + Data.session_name(table2))
           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)
diff -r 333961e15062 -r d788c11176e5 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed May 03 16:01:01 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 16:15:09 2017 +0200
@@ -103,12 +103,12 @@
 
     def ident: String = SQL.ident(name)
 
-    def sql_decl(sql_type: Type.Value => String): String =
+    def decl(sql_type: Type.Value => String): String =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
     def where_equal(s: String): String = "WHERE " + ident + " = " + string(s)
 
-    override def toString: String = sql_decl(sql_type_default)
+    override def toString: String = ident
   }
 
 
@@ -130,20 +130,17 @@
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
-    def sql_columns(sql_type: Type.Value => String): String =
+    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
     {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
           case Nil => Nil
           case keys => List("PRIMARY KEY " + enclosure(keys))
         }
-      enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
+      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
+        ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
     }
 
-    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
-      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        ident + " " + sql_columns(sql_type)
-
     def create_index(index_name: String, index_columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): String =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
@@ -162,8 +159,7 @@
       SQL.select(select_columns, distinct = distinct) + ident +
         (if (sql == "") "" else " " + sql)
 
-    override def toString: String =
-      "TABLE " + ident + " " + sql_columns(sql_type_default)
+    override def toString: String = ident
   }