--- a/src/Pure/Thy/sessions.scala Fri Apr 28 18:52:31 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Apr 28 20:03: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_statement(Session_Info.table, List(column),
+ using(db.select(Session_Info.table, 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_statement(Session_Info.table,
- Session_Info.session_name.sql_where_equal(name)))(_.execute)
- using(db.insert_statement(Session_Info.table))(stmt =>
+ using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
+ _.execute)
+ using(db.insert(Session_Info.table))(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_statement(Session_Info.table, Session_Info.build_columns,
+ using(db.select(Session_Info.table, Session_Info.build_columns,
Session_Info.session_name.sql_where_equal(name)))(stmt =>
{
val rs = stmt.executeQuery