# HG changeset patch
# User wenzelm
# Date 1473069085 -7200
# Node ID 3d723062dc7005e219aff71ca700dc4c3890a009
# Parent  af28929ff219fa70c86cd5756faf6581b58b561c
more operations;
tuned;

diff -r af28929ff219 -r 3d723062dc70 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Sep 05 11:43:37 2016 +0200
+++ b/src/Pure/General/sql.scala	Mon Sep 05 11:51:25 2016 +0200
@@ -55,7 +55,8 @@
   }
 
   abstract class Column[+A] private[SQL](
-    val name: String, val strict: Boolean, val primary_key: Boolean)
+      val name: String, val strict: Boolean, val primary_key: Boolean)
+    extends Function[ResultSet, A]
   {
     def sql_name: String = quote_ident(name)
     def sql_type: String
@@ -129,6 +130,9 @@
 
   class Table private[SQL](name: String, columns: List[Column[Any]])
   {
+    private val columns_index: Map[String, Int] =
+      columns.iterator.map(_.name).zipWithIndex.toMap
+
     Library.duplicates(columns.map(_.name)) match {
       case Nil =>
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
@@ -148,7 +152,21 @@
     def sql_drop(strict: Boolean): String =
       "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
 
+    def sql_insert: String =
+      "INSERT INTO " + quote_ident(name) +
+      " VALUES " + columns.map(_ => "?").mkString("(", ", ", ")")
+
     override def toString: String =
       "TABLE " + quote_ident(name) + " " + columns.map(_.toString).mkString("(", ", ", ")")
   }
+
+
+  /* results */
+
+  def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
+  {
+    private var _next: Boolean = rs.next()
+    def hasNext: Boolean = _next
+    def next: A = { val x = get(rs); _next = rs.next(); x }
+  }
 }
diff -r af28929ff219 -r 3d723062dc70 src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Mon Sep 05 11:43:37 2016 +0200
+++ b/src/Pure/General/sqlite.scala	Mon Sep 05 11:51:25 2016 +0200
@@ -14,6 +14,15 @@
 {
   /** database connection **/
 
+  def open_database(path: Path): Database =
+  {
+    val path0 = path.expand
+    val s0 = File.platform_path(path0)
+    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
+    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
+    new Database(path0, connection)
+  }
+
   class Database private [SQLite](path: Path, val connection: Connection)
   {
     override def toString: String = path.toString
@@ -35,37 +44,23 @@
       finally { connection.setAutoCommit(auto_commit) }
     }
 
-    def with_statement[A](sql: String)(body: PreparedStatement => A): A =
-    {
-      val stmt = connection.prepareStatement(sql)
-      try { body(stmt) } finally { stmt.close }
-    }
+
+    /* prepared statements */
+
+    def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
+
+    def insert_statement(table: SQL.Table): PreparedStatement = statement(table.sql_insert)
 
 
     /* tables */
 
+    def tables: List[String] =
+      SQL.iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
+
     def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit =
-      with_statement(table.sql_create(strict, rowid))(_.execute())
+      using(statement(table.sql_create(strict, rowid)))(_.execute())
 
     def drop_table(table: SQL.Table, strict: Boolean = true): Unit =
-      with_statement(table.sql_drop(strict))(_.execute())
-  }
-
-
-  /* open database */
-
-  def open_database(path: Path): Database =
-  {
-    val path0 = path.expand
-    val s0 = File.platform_path(path0)
-    val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
-    val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
-    new Database(path0, connection)
-  }
-
-  def with_database[A](path: Path)(body: Database => A): A =
-  {
-    val db = open_database(path)
-    try { body(db) } finally { db.close }
+      using(statement(table.sql_drop(strict)))(_.execute())
   }
 }