--- 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
- }
-}
--- 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
+ }
+}
--- 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())
-}
--- 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()) }
- }
-}
--- 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