# HG changeset patch # User wenzelm # Date 1473013883 -7200 # Node ID 163244cefb4e1ef6d5c9d8faa13d3d3690bf8326 # Parent 9da65bc756100ee43c008d23837f0edcfca3f4c1 more operations; clarified NULL treatment; diff -r 9da65bc75610 -r 163244cefb4e src/Pure/Tools/sql.scala --- a/src/Pure/Tools/sql.scala Sun Sep 04 17:38:22 2016 +0200 +++ b/src/Pure/Tools/sql.scala Sun Sep 04 20:31:23 2016 +0200 @@ -49,13 +49,22 @@ def bytes(name: String, strict: Boolean = true): Column[Bytes] = new Column_Bytes(name, strict) } - abstract class Column[A] private[SQL](val name: String, val strict: Boolean) + abstract class Column[+A] private[SQL](val name: String, val strict: Boolean) { def sql_name: String = quote_ident(name) def sql_type: String def sql_decl: String = sql_name + " " + sql_type + (if (strict) " NOT NULL" else "") - def result(rs: ResultSet): A - def result_string(rs: ResultSet): String = rs.getString(name) + def string(rs: ResultSet): String = + { + val s = rs.getString(name) + if (s == null) "" else s + } + def apply(rs: ResultSet): A + def get(rs: ResultSet): Option[A] = + { + val x = apply(rs) + if (rs.wasNull) None else Some(x) + } override def toString: String = sql_decl } @@ -64,38 +73,56 @@ extends Column[Int](name, strict) { def sql_type: String = "INTEGER" - def result(rs: ResultSet): Int = rs.getInt(name) + def apply(rs: ResultSet): Int = rs.getInt(name) } class Column_Long private[SQL](name: String, strict: Boolean) extends Column[Long](name, strict) { def sql_type: String = "INTEGER" - def result(rs: ResultSet): Long = rs.getLong(name) + def apply(rs: ResultSet): Long = rs.getLong(name) } class Column_Double private[SQL](name: String, strict: Boolean) extends Column[Double](name, strict) { def sql_type: String = "REAL" - def result(rs: ResultSet): Double = rs.getDouble(name) + def apply(rs: ResultSet): Double = rs.getDouble(name) } class Column_String private[SQL](name: String, strict: Boolean) extends Column[String](name, strict) { def sql_type: String = "TEXT" - def result(rs: ResultSet): String = rs.getString(name) + def apply(rs: ResultSet): String = + { + val s = rs.getString(name) + if (s == null) "" else s + } } class Column_Bytes private[SQL](name: String, strict: Boolean) extends Column[Bytes](name, strict) { def sql_type: String = "BLOB" - def result(rs: ResultSet): Bytes = + def apply(rs: ResultSet): Bytes = { val bs = rs.getBytes(name) - if (bs == null) null else Bytes(bs) + if (bs == null) Bytes.empty else Bytes(bs) } } + + + /* tables */ + + sealed case class Table(name: String, columns: Column[Any]*) + { + def sql_create(strict: Boolean, rowid: Boolean): String = + "CREATE TABLE " + (if (strict) "" else " IF NOT EXISTS ") + + quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") + + (if (rowid) "" else " WITHOUT ROWID") + + def sql_drop(strict: Boolean): String = + "DROP TABLE " + (if (strict) "" else " IF EXISTS ") + quote_ident(name) + } } diff -r 9da65bc75610 -r 163244cefb4e src/Pure/Tools/sqlite.scala --- a/src/Pure/Tools/sqlite.scala Sun Sep 04 17:38:22 2016 +0200 +++ b/src/Pure/Tools/sqlite.scala Sun Sep 04 20:31:23 2016 +0200 @@ -7,12 +7,12 @@ package isabelle -import java.sql.{Connection, DriverManager} +import java.sql.{DriverManager, Connection, PreparedStatement} object SQLite { - /* database connection */ + /** database connection **/ class Database private [SQLite](path: Path, val connection: Connection) { @@ -34,8 +34,26 @@ catch { case exn: Throwable => connection.rollback(savepoint); throw exn } finally { connection.setAutoCommit(auto_commit) } } + + def with_statement[A](sql: String)(body: PreparedStatement => A): A = + { + val stmt = connection.prepareStatement(sql) + try { body(stmt) } finally { stmt.close } + } + + + /* tables */ + + def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit = + with_statement(table.sql_create(strict, rowid))(_.execute()) + + def drop_table(table: SQL.Table, strict: Boolean = true): Unit = + with_statement(table.sql_drop(strict))(_.execute()) } + + /* open database */ + def open_database(path: Path): Database = { val path0 = path.expand