# HG changeset patch
# User wenzelm
# Date 1486634359 -3600
# Node ID 632bdf7b8babcac35099d7444a760d5a69c01962
# Parent  3278831c226d16903c74c8e64ea0ffea505941df
clarified modules;

diff -r 3278831c226d -r 632bdf7b8bab src/Pure/General/postgresql.scala
--- a/src/Pure/General/postgresql.scala	Wed Feb 08 22:26:10 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-/*  Title:      Pure/General/postgresql.scala
-    Author:     Makarius
-
-Support for PostgreSQL databases.
-*/
-
-package isabelle
-
-
-import java.sql.{DriverManager, Connection}
-
-
-object PostgreSQL
-{
-  val default_port = 5432
-
-  def open_database(
-    user: String,
-    password: String,
-    database: String = "",
-    host: String = "",
-    port: Int = default_port): Database =
-  {
-    require(user != "")
-
-    val spec =
-      (if (host != "") host else "localhost") +
-      (if (port != default_port) ":" + port else "") + "/" +
-      (if (database != "") database else user)
-    val connection = DriverManager.getConnection("jdbc:postgresql://" + spec, user, password)
-    new Database(spec, connection)
-  }
-
-  class Database private[PostgreSQL](spec: String, val connection: Connection) extends SQL_Database
-  {
-    override def toString: String = spec
-  }
-}
diff -r 3278831c226d -r 632bdf7b8bab src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Feb 08 22:26:10 2017 +0100
+++ b/src/Pure/General/sql.scala	Thu Feb 09 10:59:19 2017 +0100
@@ -1,17 +1,19 @@
 /*  Title:      Pure/General/sql.scala
     Author:     Makarius
 
-Generic support for SQL.
+Support for SQL databases: SQLite and PostgreSQL.
 */
 
 package isabelle
 
 
-import java.sql.ResultSet
+import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
 
 object SQL
 {
+  /** SQL language **/
+
   /* concrete syntax */
 
   def quote_char(c: Char): String =
@@ -183,4 +185,115 @@
     def hasNext: Boolean = _next
     def next: A = { val x = get(rs); _next = rs.next(); x }
   }
+
+
+
+  /** SQL database operations **/
+
+  trait 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: Table): PreparedStatement = statement(table.sql_insert)
+
+    def select_statement(table: Table, columns: List[Column[Any]],
+        sql: String = "", distinct: Boolean = false): PreparedStatement =
+      statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
+
+
+    /* tables */
+
+    def tables: List[String] =
+      iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
+
+    def create_table(table: Table, strict: Boolean = true, rowid: Boolean = true): Unit =
+      using(statement(table.sql_create(strict, rowid)))(_.execute())
+
+    def drop_table(table: Table, strict: Boolean = true): Unit =
+      using(statement(table.sql_drop(strict)))(_.execute())
+
+    def create_index(table: Table, name: String, columns: List[Column[Any]],
+        strict: Boolean = true, unique: Boolean = false): Unit =
+      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
+
+    def drop_index(table: Table, name: String, strict: Boolean = true): Unit =
+      using(statement(table.sql_drop_index(name, strict)))(_.execute())
+  }
 }
+
+
+
+/** SQLite **/
+
+object SQLite
+{
+  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) extends SQL.Database
+  {
+    override def toString: String = path.toString
+
+    def rebuild { using(statement("VACUUM"))(_.execute()) }
+  }
+}
+
+
+
+/** PostgreSQL **/
+
+object PostgreSQL
+{
+  val default_port = 5432
+
+  def open_database(
+    user: String,
+    password: String,
+    database: String = "",
+    host: String = "",
+    port: Int = default_port): Database =
+  {
+    require(user != "")
+    val spec =
+      (if (host != "") host else "localhost") +
+      (if (port != default_port) ":" + port else "") + "/" +
+      (if (database != "") database else user)
+    val connection = DriverManager.getConnection("jdbc:postgresql://" + spec, user, password)
+    new Database(spec, connection)
+  }
+
+  class Database private[PostgreSQL](spec: String, val connection: Connection) extends SQL.Database
+  {
+    override def toString: String = spec
+  }
+}
diff -r 3278831c226d -r 632bdf7b8bab src/Pure/General/sql_database.scala
--- a/src/Pure/General/sql_database.scala	Wed Feb 08 22:26:10 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-/*  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())
-}
diff -r 3278831c226d -r 632bdf7b8bab src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Wed Feb 08 22:26:10 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-/*  Title:      Pure/General/sqlite.scala
-    Author:     Makarius
-
-Support for SQLite databases.
-*/
-
-package isabelle
-
-
-import java.sql.{DriverManager, Connection}
-
-
-object SQLite
-{
-  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) extends SQL_Database
-  {
-    override def toString: String = path.toString
-
-    def rebuild { using(statement("VACUUM"))(_.execute()) }
-  }
-}
diff -r 3278831c226d -r 632bdf7b8bab src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Feb 08 22:26:10 2017 +0100
+++ b/src/Pure/build-jars	Thu Feb 09 10:59:19 2017 +0100
@@ -60,14 +60,11 @@
   General/output.scala
   General/path.scala
   General/position.scala
-  General/postgresql.scala
   General/pretty.scala
   General/properties.scala
   General/scan.scala
   General/sha1.scala
   General/sql.scala
-  General/sql_database.scala
-  General/sqlite.scala
   General/ssh.scala
   General/symbol.scala
   General/time.scala