author | wenzelm |
Wed, 08 Feb 2017 22:11:37 +0100 | |
changeset 65002 | 0c44e3e9126f |
permissions | -rw-r--r-- |
65002
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/sql_database.scala |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
3 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
4 |
General SQL database support. |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
6 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
8 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
9 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
10 |
import java.sql.{Connection, PreparedStatement} |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
11 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
12 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
13 |
trait SQL_Database |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
14 |
{ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
15 |
/* connection */ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
16 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
17 |
def connection: Connection |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
18 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
19 |
def close() { connection.close } |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
20 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
21 |
def transaction[A](body: => A): A = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
22 |
{ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
23 |
val auto_commit = connection.getAutoCommit |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
24 |
val savepoint = connection.setSavepoint |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
25 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
26 |
try { |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
27 |
connection.setAutoCommit(false) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
28 |
val result = body |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
29 |
connection.commit |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
30 |
result |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
31 |
} |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
32 |
catch { case exn: Throwable => connection.rollback(savepoint); throw exn } |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
33 |
finally { connection.setAutoCommit(auto_commit) } |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
34 |
} |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
35 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
36 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
37 |
/* statements */ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
38 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
39 |
def statement(sql: String): PreparedStatement = connection.prepareStatement(sql) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
40 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
41 |
def insert_statement(table: SQL.Table): PreparedStatement = statement(table.sql_insert) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
42 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
43 |
def select_statement(table: SQL.Table, columns: List[SQL.Column[Any]], |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
44 |
sql: String = "", distinct: Boolean = false): PreparedStatement = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
45 |
statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql)) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
46 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
47 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
48 |
/* tables */ |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
49 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
50 |
def tables: List[String] = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
51 |
SQL.iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
52 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
53 |
def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
54 |
using(statement(table.sql_create(strict, rowid)))(_.execute()) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
55 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
56 |
def drop_table(table: SQL.Table, strict: Boolean = true): Unit = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
57 |
using(statement(table.sql_drop(strict)))(_.execute()) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
58 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
59 |
def create_index(table: SQL.Table, name: String, columns: List[SQL.Column[Any]], |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
60 |
strict: Boolean = true, unique: Boolean = false): Unit = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
61 |
using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute()) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
62 |
|
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
63 |
def drop_index(table: SQL.Table, name: String, strict: Boolean = true): Unit = |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
64 |
using(statement(table.sql_drop_index(name, strict)))(_.execute()) |
0c44e3e9126f
general SQL database support, for SQLite and PostgreSQL;
wenzelm
parents:
diff
changeset
|
65 |
} |