# HG changeset patch
# User wenzelm
# Date 1493562729 -7200
# Node ID 7ef438495a0286004bf674b802844a62de51b4a9
# Parent  a5437122618282df9c4d0c423738f37f63f94e01
support for qualified names, which are not quoted (e.g. for SQLite);
more operations;

diff -r a54371226182 -r 7ef438495a02 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Apr 30 13:00:27 2017 +0200
+++ b/src/Pure/General/sql.scala	Sun Apr 30 16:32:09 2017 +0200
@@ -34,10 +34,14 @@
     "'" + s.map(escape_char(_)).mkString + "'"
 
   def quote_ident(s: String): String =
-    quote(s.replace("\"", "\"\""))
+    if (Long_Name.is_qualified(s)) s
+    else quote(s.replace("\"", "\"\""))
 
   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 "
+
 
   /* types */
 
@@ -87,6 +91,9 @@
   sealed case class Column(
     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
   {
+    def apply(table: Table): Column =
+      Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
+
     def sql_name: String = quote_ident(name)
     def sql_decl(sql_type: Type.Value => String): String =
       sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
@@ -143,9 +150,8 @@
     def sql_delete: String =
       "DELETE FROM " + quote_ident(name)
 
-    def sql_select(select_columns: List[Column], distinct: Boolean): String =
-      "SELECT " + (if (distinct) "DISTINCT " else "") +
-      commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
+    def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
+      select(select_columns, distinct = distinct) + quote_ident(name)
 
     override def toString: String =
       "TABLE " + quote_ident(name) + " " + sql_columns(sql_type_default)
@@ -205,7 +211,7 @@
 
     def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
         : PreparedStatement =
-      statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
+      statement(table.sql_select(columns, distinct = distinct) + (if (sql == "") "" else " " + sql))
 
 
     /* input */