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