src/Pure/Thy/sessions.scala
changeset 65699 9f74d9aa0bdf
parent 65698 38139b2067cf
child 65740 83388f09e9ab
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed May 03 15:51:34 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed May 03 15:53:23 2017 +0200
     1.3 @@ -764,7 +764,7 @@
     1.4  
     1.5      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
     1.6        db.using_statement(Session_Info.table.select(List(column),
     1.7 -        Session_Info.session_name.sql_where_equal(name)))(stmt =>
     1.8 +        Session_Info.session_name.where_equal(name)))(stmt =>
     1.9        {
    1.10          val rs = stmt.executeQuery
    1.11          if (!rs.next) Bytes.empty else db.bytes(rs, column)
    1.12 @@ -822,7 +822,7 @@
    1.13        db.transaction {
    1.14          db.create_table(Session_Info.table)
    1.15          db.using_statement(
    1.16 -          Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
    1.17 +          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.18          db.using_statement(Session_Info.table.insert())(stmt =>
    1.19          {
    1.20            db.set_string(stmt, 1, name)
    1.21 @@ -865,7 +865,7 @@
    1.22  
    1.23      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.24        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.25 -        Session_Info.session_name.sql_where_equal(name)))(stmt =>
    1.26 +        Session_Info.session_name.where_equal(name)))(stmt =>
    1.27        {
    1.28          val rs = stmt.executeQuery
    1.29          if (!rs.next) None