general SQL database support, for SQLite and PostgreSQL;
tuned;

--- a/src/Pure/General/postgresql.scala	Wed Feb 08 21:06:47 2017 +0100
+++ b/src/Pure/General/postgresql.scala	Wed Feb 08 22:11:37 2017 +0100
@@ -12,9 +12,6 @@
 
 object PostgreSQL
 {
-  /** database connection **/
-
-  val default_host = "localhost"
   val default_port = 5432
 
   def open_database(
@@ -34,7 +31,7 @@
     new Database(spec, connection)
   }
 
-  class Database private[PostgreSQL](spec: String, val connection: Connection)
+  class Database private[PostgreSQL](spec: String, val connection: Connection) extends SQL_Database
   {
     override def toString: String = spec
   }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sql_database.scala	Wed Feb 08 22:11:37 2017 +0100
@@ -0,0 +1,65 @@
+/*  Title:      Pure/General/sql_database.scala
+    Author:     Makarius
+
+General SQL database support.
+*/
+
+package isabelle
+
+
+import java.sql.{Connection, PreparedStatement}
+
+
+trait SQL_Database
+{
+  /* connection */
+
+  def connection: Connection
+
+  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) }
+  }
+
+
+  /* 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 */
+
+  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 =
+    using(statement(table.sql_create(strict, rowid)))(_.execute())
+
+  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())
+}

--- a/src/Pure/General/sqlite.scala	Wed Feb 08 21:06:47 2017 +0100
+++ b/src/Pure/General/sqlite.scala	Wed Feb 08 22:11:37 2017 +0100
@@ -7,13 +7,11 @@
 package isabelle
 
 
-import java.sql.{DriverManager, Connection, PreparedStatement}
+import java.sql.{DriverManager, Connection}
 
 
 object SQLite
 {
-  /** database connection **/
-
   def open_database(path: Path): Database =
   {
     val path0 = path.expand
@@ -23,57 +21,10 @@
     new Database(path0, connection)
   }
 
-  class Database private[SQLite](path: Path, val connection: Connection)
+  class Database private[SQLite](path: Path, val connection: Connection) extends SQL_Database
   {
     override def toString: String = path.toString
 
-    def close() { connection.close }
-
     def rebuild { using(statement("VACUUM"))(_.execute()) }
-
-    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) }
-    }
-
-
-    /* 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 */
-
-    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 =
-      using(statement(table.sql_create(strict, rowid)))(_.execute())
-
-    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())
   }
 }

--- a/src/Pure/build-jars	Wed Feb 08 21:06:47 2017 +0100
+++ b/src/Pure/build-jars	Wed Feb 08 22:11:37 2017 +0100
@@ -66,6 +66,7 @@
   General/scan.scala
   General/sha1.scala
   General/sql.scala
+  General/sql_database.scala
   General/sqlite.scala
   General/ssh.scala
   General/symbol.scala