src/Pure/Thy/sessions.scala
changeset 65740 83388f09e9ab
parent 65699 9f74d9aa0bdf
child 65748 1f4a80e80c88
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat May 06 11:43:43 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 06 12:45:42 2017 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  import java.nio.ByteBuffer
     1.5  import java.nio.channels.FileChannel
     1.6  import java.nio.file.StandardOpenOption
     1.7 -import java.sql.PreparedStatement
     1.8  
     1.9  import scala.collection.SortedSet
    1.10  import scala.collection.mutable
    1.11 @@ -766,8 +765,8 @@
    1.12        db.using_statement(Session_Info.table.select(List(column),
    1.13          Session_Info.session_name.where_equal(name)))(stmt =>
    1.14        {
    1.15 -        val rs = stmt.executeQuery
    1.16 -        if (!rs.next) Bytes.empty else db.bytes(rs, column)
    1.17 +        val res = stmt.execute_query()
    1.18 +        if (!res.next()) Bytes.empty else res.bytes(column)
    1.19        })
    1.20  
    1.21      def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    1.22 @@ -825,15 +824,15 @@
    1.23            Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.24          db.using_statement(Session_Info.table.insert())(stmt =>
    1.25          {
    1.26 -          db.set_string(stmt, 1, name)
    1.27 -          db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    1.28 -          db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
    1.29 -          db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
    1.30 -          db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
    1.31 -          db.set_string(stmt, 6, cat_lines(build.sources))
    1.32 -          db.set_string(stmt, 7, cat_lines(build.input_heaps))
    1.33 -          db.set_string(stmt, 8, build.output_heap getOrElse "")
    1.34 -          db.set_int(stmt, 9, build.return_code)
    1.35 +          stmt.set_string(1, name)
    1.36 +          stmt.set_bytes(2, encode_properties(build_log.session_timing))
    1.37 +          stmt.set_bytes(3, compress_properties(build_log.command_timings))
    1.38 +          stmt.set_bytes(4, compress_properties(build_log.ml_statistics))
    1.39 +          stmt.set_bytes(5, compress_properties(build_log.task_statistics))
    1.40 +          stmt.set_string(6, cat_lines(build.sources))
    1.41 +          stmt.set_string(7, cat_lines(build.input_heaps))
    1.42 +          stmt.set_string(8, build.output_heap getOrElse "")
    1.43 +          stmt.set_int(9, build.return_code)
    1.44            stmt.execute()
    1.45          })
    1.46        }
    1.47 @@ -867,15 +866,15 @@
    1.48        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.49          Session_Info.session_name.where_equal(name)))(stmt =>
    1.50        {
    1.51 -        val rs = stmt.executeQuery
    1.52 -        if (!rs.next) None
    1.53 +        val res = stmt.execute_query()
    1.54 +        if (!res.next()) None
    1.55          else {
    1.56            Some(
    1.57              Build.Session_Info(
    1.58 -              split_lines(db.string(rs, Session_Info.sources)),
    1.59 -              split_lines(db.string(rs, Session_Info.input_heaps)),
    1.60 -              db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.61 -              db.int(rs, Session_Info.return_code)))
    1.62 +              split_lines(res.string(Session_Info.sources)),
    1.63 +              split_lines(res.string(Session_Info.input_heaps)),
    1.64 +              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.65 +              res.int(Session_Info.return_code)))
    1.66          }
    1.67        })
    1.68    }