src/Pure/General/sqlite.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sqlite.scala	Mon Sep 05 10:34:45 2016 +0200
@@ -0,0 +1,71 @@
+/*  Title:      Pure/General/sqlite.scala
+    Author:     Makarius
+
+Support for SQLite databases.
+*/
+
+package isabelle
+
+
+import java.sql.{DriverManager, Connection, PreparedStatement}
+
+
+object SQLite
+{
+  /** database connection **/
+
+  class Database private [SQLite](path: Path, val connection: Connection)
+  {
+    override def toString: String = path.toString
+
+    def close { connection.close }
+
+    def transaction[A](body: => A): A =
+    {
+      val auto_commit = connection.getAutoCommit
+      val savepoint = connection.setSavepoint
+
+      try {
+        connection.setAutoCommit(false)
+        val result = body
+        connection.commit
+        result
+      }
+      catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
+      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 }
+    }
+
+
+    /* tables */
+
+    def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit =
+      with_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 }
+  }
+}