src/Pure/Thy/sessions.scala
changeset 65619 e33b3d57b7cb
parent 65604 637aa8e93cd7
child 65698 38139b2067cf
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 28 18:52:31 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 20:03:34 2017 +0200
     1.3 @@ -763,7 +763,7 @@
     1.4      /* SQL database content */
     1.5  
     1.6      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
     1.7 -      using(db.select_statement(Session_Info.table, List(column),
     1.8 +      using(db.select(Session_Info.table, List(column),
     1.9          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    1.10        {
    1.11          val rs = stmt.executeQuery
    1.12 @@ -821,9 +821,9 @@
    1.13      {
    1.14        db.transaction {
    1.15          db.create_table(Session_Info.table)
    1.16 -        using(db.delete_statement(Session_Info.table,
    1.17 -          Session_Info.session_name.sql_where_equal(name)))(_.execute)
    1.18 -        using(db.insert_statement(Session_Info.table))(stmt =>
    1.19 +        using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
    1.20 +          _.execute)
    1.21 +        using(db.insert(Session_Info.table))(stmt =>
    1.22          {
    1.23            db.set_string(stmt, 1, name)
    1.24            db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    1.25 @@ -864,7 +864,7 @@
    1.26      }
    1.27  
    1.28      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.29 -      using(db.select_statement(Session_Info.table, Session_Info.build_columns,
    1.30 +      using(db.select(Session_Info.table, Session_Info.build_columns,
    1.31          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    1.32        {
    1.33          val rs = stmt.executeQuery