--- a/src/Pure/Admin/build_log.scala Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Wed May 03 15:51:34 2017 +0200
@@ -704,11 +704,11 @@
val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)
def recent(table: SQL.Table, days: Int): String =
- table.sql_select(table.columns) +
+ table.select(table.columns) +
" WHERE " + pull_date(table).ident + " > now() - INTERVAL '" + days.max(0) + " days'"
def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
- table.sql_select(columns) +
+ table.select(columns) +
" INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
" ON " + Prop.isabelle_version(table).ident + " = recent." + Prop.isabelle_version.ident
}
@@ -761,9 +761,9 @@
List(Data.isabelle_pull_date_table, Data.afp_pull_date_table).foreach(table =>
{
db2.create_table(table)
- using(db2.insert(table))(stmt2 =>
+ db2.using_statement(table.insert())(stmt2 =>
{
- using(db.statement(Data.recent(table, days)))(stmt =>
+ db.using_statement(Data.recent(table, days))(stmt =>
{
val rs = stmt.executeQuery
while (rs.next()) {
@@ -780,7 +780,7 @@
}
def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
- using(db.select(table, List(column), distinct = true))(stmt =>
+ db.using_statement(table.select(List(column), distinct = true))(stmt =>
SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
def update_meta_info(db: SQL.Database, log_file: Log_File)
@@ -789,8 +789,8 @@
val table = Data.meta_info_table
db.transaction {
- using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
- using(db.insert(table))(stmt =>
+ db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+ db.using_statement(table.insert())(stmt =>
{
db.set_string(stmt, 1, log_file.name)
for ((c, i) <- table.columns.tail.zipWithIndex) {
@@ -810,8 +810,8 @@
val table = Data.sessions_table
db.transaction {
- using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
- using(db.insert(table))(stmt =>
+ db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+ db.using_statement(table.insert())(stmt =>
{
val entries_iterator =
if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
@@ -844,8 +844,8 @@
val table = Data.ml_statistics_table
db.transaction {
- using(db.delete(table, Data.log_name.sql_where_equal(log_file.name)))(_.execute)
- using(db.insert(table))(stmt =>
+ db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+ db.using_statement(table.insert())(stmt =>
{
val ml_stats: List[(String, Option[Bytes])] =
Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
@@ -896,7 +896,7 @@
{
val table = Data.meta_info_table
val columns = table.columns.tail
- using(db.select(table, columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
+ db.using_statement(table.select(columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
{
val rs = stmt.executeQuery
if (!rs.next) None
@@ -949,7 +949,7 @@
else (columns1, table1.ident)
val sessions =
- using(db.statement(SQL.select(columns) + from + " " + where))(stmt =>
+ db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
{
SQL.iterator(stmt.executeQuery)(rs =>
{
--- a/src/Pure/General/sql.scala Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/General/sql.scala Wed May 03 15:51:34 2017 +0200
@@ -141,23 +141,27 @@
enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
}
- def sql_create(strict: Boolean, sql_type: Type.Value => String): String =
+ def create(strict: Boolean = false, sql_type: Type.Value => String): String =
"CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
ident + " " + sql_columns(sql_type)
- def sql_create_index(
- index_name: String, index_columns: List[Column],
- strict: Boolean, unique: Boolean): String =
+ def create_index(index_name: String, index_columns: List[Column],
+ strict: Boolean = false, unique: Boolean = false): String =
"CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
(if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
ident + " " + enclosure(index_columns.map(_.name))
- def sql_insert: String = "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?"))
+ def insert(sql: String = ""): String =
+ "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
+ (if (sql == "") "" else " " + sql)
- def sql_delete: String = "DELETE FROM " + ident
+ def delete(sql: String = ""): String =
+ "DELETE FROM " + ident +
+ (if (sql == "") "" else " " + sql)
- def sql_select(select_columns: List[Column], distinct: Boolean = false): String =
- select(select_columns, distinct = distinct) + ident
+ def select(select_columns: List[Column], sql: String = "", distinct: Boolean = false): String =
+ SQL.select(select_columns, distinct = distinct) + ident +
+ (if (sql == "") "" else " " + sql)
override def toString: String =
"TABLE " + ident + " " + sql_columns(sql_type_default)
@@ -208,16 +212,11 @@
/* statements */
- def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
-
- def insert(table: Table): PreparedStatement = statement(table.sql_insert)
+ def statement(sql: String): PreparedStatement =
+ connection.prepareStatement(sql)
- def delete(table: Table, sql: String = ""): PreparedStatement =
- statement(table.sql_delete + (if (sql == "") "" else " " + sql))
-
- def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
- : PreparedStatement =
- statement(table.sql_select(columns, distinct = distinct) + (if (sql == "") "" else " " + sql))
+ def using_statement[A](sql: String)(f: PreparedStatement => A): A =
+ using(statement(sql))(f)
/* input */
@@ -305,18 +304,18 @@
iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
- using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
- _.execute())
+ using_statement(
+ table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
def create_index(table: Table, name: String, columns: List[Column],
strict: Boolean = false, unique: Boolean = false): Unit =
- using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
+ using_statement(table.create_index(name, columns, strict, unique))(_.execute())
def create_view(table: Table, strict: Boolean = false): Unit =
{
if (strict || !tables.contains(table.name)) {
val sql = "CREATE VIEW " + table.ident + " AS " + table.expr
- using(statement(sql))(_.execute())
+ using_statement(sql)(_.execute())
}
}
}
@@ -356,7 +355,7 @@
def date(rs: ResultSet, column: SQL.Column): Date =
date_format.parse(string(rs, column))
- def rebuild { using(statement("VACUUM"))(_.execute()) }
+ def rebuild { using_statement("VACUUM")(_.execute()) }
}
}
--- a/src/Pure/Thy/sessions.scala Wed May 03 15:24:24 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Wed May 03 15:51:34 2017 +0200
@@ -763,7 +763,7 @@
/* SQL database content */
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
- using(db.select(Session_Info.table, List(column),
+ db.using_statement(Session_Info.table.select(List(column),
Session_Info.session_name.sql_where_equal(name)))(stmt =>
{
val rs = stmt.executeQuery
@@ -821,9 +821,9 @@
{
db.transaction {
db.create_table(Session_Info.table)
- using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
- _.execute)
- using(db.insert(Session_Info.table))(stmt =>
+ db.using_statement(
+ Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
+ db.using_statement(Session_Info.table.insert())(stmt =>
{
db.set_string(stmt, 1, name)
db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
@@ -864,7 +864,7 @@
}
def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
- using(db.select(Session_Info.table, Session_Info.build_columns,
+ db.using_statement(Session_Info.table.select(Session_Info.build_columns,
Session_Info.session_name.sql_where_equal(name)))(stmt =>
{
val rs = stmt.executeQuery