src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Mon Sep 05 11:51:25 2016 +0200
+++ b/src/Pure/General/sql.scala	Mon Sep 05 15:00:32 2016 +0200
@@ -37,6 +37,8 @@
     "`" + s + "`"
   }
 
+  def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
+
 
   /* columns */
 
@@ -126,7 +128,7 @@
 
   /* tables */
 
-  def table(name: String, columns: Column[Any]*): Table = new Table(name, columns.toList)
+  def table(name: String, columns: List[Column[Any]]): Table = new Table(name, columns)
 
   class Table private[SQL](name: String, columns: List[Column[Any]])
   {
@@ -146,18 +148,31 @@
 
     def sql_create(strict: Boolean, rowid: Boolean): String =
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") +
+        quote_ident(name) + " " + enclosure(columns.map(_.sql_decl)) +
         (if (rowid) "" else " WITHOUT ROWID")
 
     def sql_drop(strict: Boolean): String =
       "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
 
+    def sql_create_index(
+        index_name: String, index_columns: List[Column[Any]],
+        strict: Boolean, unique: Boolean): String =
+      "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
+        (if (strict) "" else "IF NOT EXISTS ") + quote_ident(index_name) + " ON " +
+        quote_ident(name) + " " + enclosure(index_columns.map(_.name))
+
+    def sql_drop_index(index_name: String, strict: Boolean): String =
+      "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name)
+
     def sql_insert: String =
-      "INSERT INTO " + quote_ident(name) +
-      " VALUES " + columns.map(_ => "?").mkString("(", ", ", ")")
+      "INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?"))
+
+    def sql_select(select_columns: List[Column[Any]], distinct: Boolean): String =
+      "SELECT " + (if (distinct) "DISTINCT " else "") +
+      commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
 
     override def toString: String =
-      "TABLE " + quote_ident(name) + " " + columns.map(_.toString).mkString("(", ", ", ")")
+      "TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString))
   }