# HG changeset patch
# User wenzelm
# Date 1473080432 -7200
# Node ID c6cbdfaae19eb24acbf2a031a96173728996969a
# Parent  3d723062dc7005e219aff71ca700dc4c3890a009
more operations;

diff -r 3d723062dc70 -r c6cbdfaae19e 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))
   }
 
 
diff -r 3d723062dc70 -r c6cbdfaae19e src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Mon Sep 05 11:51:25 2016 +0200
+++ b/src/Pure/General/sqlite.scala	Mon Sep 05 15:00:32 2016 +0200
@@ -45,12 +45,16 @@
     }
 
 
-    /* prepared statements */
+    /* statements */
 
     def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
 
     def insert_statement(table: SQL.Table): PreparedStatement = statement(table.sql_insert)
 
+    def select_statement(table: SQL.Table, columns: List[SQL.Column[Any]],
+        sql: String = "", distinct: Boolean = false): PreparedStatement =
+      statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
+
 
     /* tables */
 
@@ -62,5 +66,12 @@
 
     def drop_table(table: SQL.Table, strict: Boolean = true): Unit =
       using(statement(table.sql_drop(strict)))(_.execute())
+
+    def create_index(table: SQL.Table, name: String, columns: List[SQL.Column[Any]],
+        strict: Boolean = true, unique: Boolean = false): Unit =
+      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
+
+    def drop_index(table: SQL.Table, name: String, strict: Boolean = true): Unit =
+      using(statement(table.sql_drop_index(name, strict)))(_.execute())
   }
 }