|
1 /* Title: Pure/General/sqlite.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for SQLite databases. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.sql.{DriverManager, Connection, PreparedStatement} |
|
11 |
|
12 |
|
13 object SQLite |
|
14 { |
|
15 /** database connection **/ |
|
16 |
|
17 class Database private [SQLite](path: Path, val connection: Connection) |
|
18 { |
|
19 override def toString: String = path.toString |
|
20 |
|
21 def close { connection.close } |
|
22 |
|
23 def transaction[A](body: => A): A = |
|
24 { |
|
25 val auto_commit = connection.getAutoCommit |
|
26 val savepoint = connection.setSavepoint |
|
27 |
|
28 try { |
|
29 connection.setAutoCommit(false) |
|
30 val result = body |
|
31 connection.commit |
|
32 result |
|
33 } |
|
34 catch { case exn: Throwable => connection.rollback(savepoint); throw exn } |
|
35 finally { connection.setAutoCommit(auto_commit) } |
|
36 } |
|
37 |
|
38 def with_statement[A](sql: String)(body: PreparedStatement => A): A = |
|
39 { |
|
40 val stmt = connection.prepareStatement(sql) |
|
41 try { body(stmt) } finally { stmt.close } |
|
42 } |
|
43 |
|
44 |
|
45 /* tables */ |
|
46 |
|
47 def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit = |
|
48 with_statement(table.sql_create(strict, rowid))(_.execute()) |
|
49 |
|
50 def drop_table(table: SQL.Table, strict: Boolean = true): Unit = |
|
51 with_statement(table.sql_drop(strict))(_.execute()) |
|
52 } |
|
53 |
|
54 |
|
55 /* open database */ |
|
56 |
|
57 def open_database(path: Path): Database = |
|
58 { |
|
59 val path0 = path.expand |
|
60 val s0 = File.platform_path(path0) |
|
61 val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0 |
|
62 val connection = DriverManager.getConnection("jdbc:sqlite:" + s1) |
|
63 new Database(path0, connection) |
|
64 } |
|
65 |
|
66 def with_database[A](path: Path)(body: Database => A): A = |
|
67 { |
|
68 val db = open_database(path) |
|
69 try { body(db) } finally { db.close } |
|
70 } |
|
71 } |