clarified signature;
authorwenzelm
Sat May 06 12:45:42 2017 +0200 (2017-05-06)
changeset 6574083388f09e9ab
parent 65739 3f206cfca625
child 65741 cf42659364c9
clarified signature;
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_stats.scala
src/Pure/General/sql.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Sat May 06 11:43:43 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Sat May 06 12:45:42 2017 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  import java.time.ZoneId
     1.5  import java.time.format.{DateTimeFormatter, DateTimeParseException}
     1.6  import java.util.Locale
     1.7 -import java.sql.PreparedStatement
     1.8  
     1.9  import scala.collection.immutable.SortedMap
    1.10  import scala.collection.mutable
    1.11 @@ -781,8 +780,8 @@
    1.12              val recent_log_names =
    1.13                db.using_statement(
    1.14                  Data.select_recent(
    1.15 -                  Data.meta_info_table, List(Data.log_name), days, distinct = true))(
    1.16 -                    stmt => SQL.iterator(stmt.executeQuery)(db.string(_, Data.log_name)).toList)
    1.17 +                  Data.meta_info_table, List(Data.log_name), days, distinct = true))(stmt =>
    1.18 +                    stmt.execute_query().iterator(_.string(Data.log_name)).toList)
    1.19  
    1.20              for (log_name <- recent_log_names) {
    1.21                read_meta_info(db, log_name).foreach(meta_info =>
    1.22 @@ -802,11 +801,11 @@
    1.23                {
    1.24                  db.using_statement(Data.recent_table(days).query)(stmt =>
    1.25                  {
    1.26 -                  val rs = stmt.executeQuery
    1.27 -                  while (rs.next()) {
    1.28 +                  val res = stmt.execute_query()
    1.29 +                  while (res.next()) {
    1.30                      for ((c, i) <- table.columns.zipWithIndex)
    1.31 -                      db2.set_string(stmt2, i + 1, db.get_string(rs, c))
    1.32 -                    stmt2.execute
    1.33 +                      stmt2.set_string(i + 1, res.get_string(c))
    1.34 +                    stmt2.execute()
    1.35                    }
    1.36                  })
    1.37                })
    1.38 @@ -822,19 +821,19 @@
    1.39  
    1.40      def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
    1.41        db.using_statement(table.select(List(column), distinct = true))(stmt =>
    1.42 -        SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
    1.43 +        stmt.execute_query().iterator(_.string(column)).toSet)
    1.44  
    1.45      def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
    1.46      {
    1.47        val table = Data.meta_info_table
    1.48        db.using_statement(db.insert_permissive(table))(stmt =>
    1.49        {
    1.50 -        db.set_string(stmt, 1, log_name)
    1.51 +        stmt.set_string(1, log_name)
    1.52          for ((c, i) <- table.columns.tail.zipWithIndex) {
    1.53            if (c.T == SQL.Type.Date)
    1.54 -            db.set_date(stmt, i + 2, meta_info.get_date(c))
    1.55 +            stmt.set_date(i + 2, meta_info.get_date(c))
    1.56            else
    1.57 -            db.set_string(stmt, i + 2, meta_info.get(c))
    1.58 +            stmt.set_string(i + 2, meta_info.get(c))
    1.59          }
    1.60          stmt.execute()
    1.61        })
    1.62 @@ -849,21 +848,21 @@
    1.63            if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
    1.64            else build_info.sessions.iterator
    1.65          for ((session_name, session) <- entries_iterator) {
    1.66 -          db.set_string(stmt, 1, log_name)
    1.67 -          db.set_string(stmt, 2, session_name)
    1.68 -          db.set_string(stmt, 3, session.proper_chapter)
    1.69 -          db.set_string(stmt, 4, session.proper_groups)
    1.70 -          db.set_int(stmt, 5, session.threads)
    1.71 -          db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
    1.72 -          db.set_long(stmt, 7, session.timing.cpu.proper_ms)
    1.73 -          db.set_long(stmt, 8, session.timing.gc.proper_ms)
    1.74 -          db.set_double(stmt, 9, session.timing.factor)
    1.75 -          db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
    1.76 -          db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
    1.77 -          db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
    1.78 -          db.set_double(stmt, 13, session.ml_timing.factor)
    1.79 -          db.set_long(stmt, 14, session.heap_size)
    1.80 -          db.set_string(stmt, 15, session.status.map(_.toString))
    1.81 +          stmt.set_string(1, log_name)
    1.82 +          stmt.set_string(2, session_name)
    1.83 +          stmt.set_string(3, session.proper_chapter)
    1.84 +          stmt.set_string(4, session.proper_groups)
    1.85 +          stmt.set_int(5, session.threads)
    1.86 +          stmt.set_long(6, session.timing.elapsed.proper_ms)
    1.87 +          stmt.set_long(7, session.timing.cpu.proper_ms)
    1.88 +          stmt.set_long(8, session.timing.gc.proper_ms)
    1.89 +          stmt.set_double(9, session.timing.factor)
    1.90 +          stmt.set_long(10, session.ml_timing.elapsed.proper_ms)
    1.91 +          stmt.set_long(11, session.ml_timing.cpu.proper_ms)
    1.92 +          stmt.set_long(12, session.ml_timing.gc.proper_ms)
    1.93 +          stmt.set_double(13, session.ml_timing.factor)
    1.94 +          stmt.set_long(14, session.heap_size)
    1.95 +          stmt.set_string(15, session.status.map(_.toString))
    1.96            stmt.execute()
    1.97          }
    1.98        })
    1.99 @@ -880,9 +879,9 @@
   1.100              build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
   1.101          val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
   1.102          for ((session_name, ml_statistics) <- entries) {
   1.103 -          db.set_string(stmt, 1, log_name)
   1.104 -          db.set_string(stmt, 2, session_name)
   1.105 -          db.set_bytes(stmt, 3, ml_statistics)
   1.106 +          stmt.set_string(1, log_name)
   1.107 +          stmt.set_string(2, session_name)
   1.108 +          stmt.set_bytes(3, ml_statistics)
   1.109            stmt.execute()
   1.110          }
   1.111        })
   1.112 @@ -936,15 +935,15 @@
   1.113        val columns = table.columns.tail
   1.114        db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
   1.115        {
   1.116 -        val rs = stmt.executeQuery
   1.117 -        if (!rs.next) None
   1.118 +        val res = stmt.execute_query()
   1.119 +        if (!res.next) None
   1.120          else {
   1.121            val results =
   1.122              columns.map(c => c.name ->
   1.123                (if (c.T == SQL.Type.Date)
   1.124 -                db.get_date(rs, c).map(Log_File.Date_Format(_))
   1.125 +                res.get_date(c).map(Log_File.Date_Format(_))
   1.126                 else
   1.127 -                db.get_string(rs, c)))
   1.128 +                res.get_string(c)))
   1.129            val n = Prop.all_props.length
   1.130            val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
   1.131            val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
   1.132 @@ -987,26 +986,28 @@
   1.133        val sessions =
   1.134          db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
   1.135          {
   1.136 -          SQL.iterator(stmt.executeQuery)(rs =>
   1.137 +          stmt.execute_query().iterator(res =>
   1.138            {
   1.139 -            val session_name = db.string(rs, Data.session_name)
   1.140 +            val session_name = res.string(Data.session_name)
   1.141              val session_entry =
   1.142                Session_Entry(
   1.143 -                chapter = db.string(rs, Data.chapter),
   1.144 -                groups = split_lines(db.string(rs, Data.groups)),
   1.145 -                threads = db.get_int(rs, Data.threads),
   1.146 +                chapter = res.string(Data.chapter),
   1.147 +                groups = split_lines(res.string(Data.groups)),
   1.148 +                threads = res.get_int(Data.threads),
   1.149                  timing =
   1.150 -                  Timing(Time.ms(db.long(rs, Data.timing_elapsed)),
   1.151 -                    Time.ms(db.long(rs, Data.timing_cpu)),
   1.152 -                    Time.ms(db.long(rs, Data.timing_gc))),
   1.153 +                  Timing(
   1.154 +                    Time.ms(res.long(Data.timing_elapsed)),
   1.155 +                    Time.ms(res.long(Data.timing_cpu)),
   1.156 +                    Time.ms(res.long(Data.timing_gc))),
   1.157                  ml_timing =
   1.158 -                  Timing(Time.ms(db.long(rs, Data.ml_timing_elapsed)),
   1.159 -                    Time.ms(db.long(rs, Data.ml_timing_cpu)),
   1.160 -                    Time.ms(db.long(rs, Data.ml_timing_gc))),
   1.161 -                heap_size = db.get_long(rs, Data.heap_size),
   1.162 -                status = db.get_string(rs, Data.status).map(Session_Status.withName(_)),
   1.163 +                  Timing(
   1.164 +                    Time.ms(res.long(Data.ml_timing_elapsed)),
   1.165 +                    Time.ms(res.long(Data.ml_timing_cpu)),
   1.166 +                    Time.ms(res.long(Data.ml_timing_gc))),
   1.167 +                heap_size = res.get_long(Data.heap_size),
   1.168 +                status = res.get_string(Data.status).map(Session_Status.withName(_)),
   1.169                  ml_statistics =
   1.170 -                  if (ml_statistics) uncompress_properties(db.bytes(rs, Data.ml_statistics))
   1.171 +                  if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics))
   1.172                    else Nil)
   1.173              session_name -> session_entry
   1.174            }).toMap
     2.1 --- a/src/Pure/Admin/build_stats.scala	Sat May 06 11:43:43 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_stats.scala	Sat May 06 12:45:42 2017 +0200
     2.3 @@ -79,26 +79,26 @@
     2.4  
     2.5          db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
     2.6          {
     2.7 -          val rs = stmt.executeQuery
     2.8 -          while (rs.next) {
     2.9 -            val ml_platform = db.string(rs, Build_Log.Settings.ML_PLATFORM)
    2.10 -            val threads = db.get_int(rs, Build_Log.Data.threads)
    2.11 +          val res = stmt.execute_query()
    2.12 +          while (res.next()) {
    2.13 +            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    2.14 +            val threads = res.get_int(Build_Log.Data.threads)
    2.15              val name =
    2.16                profile.name +
    2.17                  "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
    2.18                  "_M" + threads.getOrElse(1)
    2.19  
    2.20 -            val session = db.string(rs, Build_Log.Data.session_name)
    2.21 +            val session = res.string(Build_Log.Data.session_name)
    2.22              val entry =
    2.23 -              Entry(db.date(rs, Build_Log.Data.pull_date),
    2.24 +              Entry(res.date(Build_Log.Data.pull_date),
    2.25                  Timing(
    2.26 -                  Time.ms(db.long(rs, Build_Log.Data.timing_elapsed)),
    2.27 -                  Time.ms(db.long(rs, Build_Log.Data.timing_cpu)),
    2.28 -                  Time.ms(db.long(rs, Build_Log.Data.timing_gc))),
    2.29 +                  Time.ms(res.long(Build_Log.Data.timing_elapsed)),
    2.30 +                  Time.ms(res.long(Build_Log.Data.timing_cpu)),
    2.31 +                  Time.ms(res.long(Build_Log.Data.timing_gc))),
    2.32                  Timing(
    2.33 -                  Time.ms(db.long(rs, Build_Log.Data.ml_timing_elapsed)),
    2.34 -                  Time.ms(db.long(rs, Build_Log.Data.ml_timing_cpu)),
    2.35 -                  Time.ms(db.long(rs, Build_Log.Data.ml_timing_gc))))
    2.36 +                  Time.ms(res.long(Build_Log.Data.ml_timing_elapsed)),
    2.37 +                  Time.ms(res.long(Build_Log.Data.ml_timing_cpu)),
    2.38 +                  Time.ms(res.long(Build_Log.Data.ml_timing_gc))))
    2.39  
    2.40              val session_entries = data.getOrElse(name, Map.empty)
    2.41              val entries = session_entries.getOrElse(session, Nil)
     3.1 --- a/src/Pure/General/sql.scala	Sat May 06 11:43:43 2017 +0200
     3.2 +++ b/src/Pure/General/sql.scala	Sat May 06 12:45:42 2017 +0200
     3.3 @@ -9,6 +9,8 @@
     3.4  import java.time.OffsetDateTime
     3.5  import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
     3.6  
     3.7 +import scala.collection.mutable
     3.8 +
     3.9  
    3.10  object SQL
    3.11  {
    3.12 @@ -166,17 +168,114 @@
    3.13  
    3.14    /** SQL database operations **/
    3.15  
    3.16 +  /* statements */
    3.17 +
    3.18 +  class Statement private[SQL](val db: Database, val rep: PreparedStatement)
    3.19 +  {
    3.20 +    stmt =>
    3.21 +
    3.22 +    def set_bool(i: Int, x: Boolean) { rep.setBoolean(i, x) }
    3.23 +    def set_bool(i: Int, x: Option[Boolean])
    3.24 +    {
    3.25 +      if (x.isDefined) set_bool(i, x.get)
    3.26 +      else rep.setNull(i, java.sql.Types.BOOLEAN)
    3.27 +    }
    3.28 +
    3.29 +    def set_int(i: Int, x: Int) { rep.setInt(i, x) }
    3.30 +    def set_int(i: Int, x: Option[Int])
    3.31 +    {
    3.32 +      if (x.isDefined) set_int(i, x.get)
    3.33 +      else rep.setNull(i, java.sql.Types.INTEGER)
    3.34 +    }
    3.35 +
    3.36 +    def set_long(i: Int, x: Long) { rep.setLong(i, x) }
    3.37 +    def set_long(i: Int, x: Option[Long])
    3.38 +    {
    3.39 +      if (x.isDefined) set_long(i, x.get)
    3.40 +      else rep.setNull(i, java.sql.Types.BIGINT)
    3.41 +    }
    3.42 +
    3.43 +    def set_double(i: Int, x: Double) { rep.setDouble(i, x) }
    3.44 +    def set_double(i: Int, x: Option[Double])
    3.45 +    {
    3.46 +      if (x.isDefined) set_double(i, x.get)
    3.47 +      else rep.setNull(i, java.sql.Types.DOUBLE)
    3.48 +    }
    3.49 +
    3.50 +    def set_string(i: Int, x: String) { rep.setString(i, x) }
    3.51 +    def set_string(i: Int, x: Option[String]): Unit = set_string(i, x.orNull)
    3.52 +
    3.53 +    def set_bytes(i: Int, bytes: Bytes)
    3.54 +    {
    3.55 +      if (bytes == null) rep.setBytes(i, null)
    3.56 +      else rep.setBinaryStream(i, bytes.stream(), bytes.length)
    3.57 +    }
    3.58 +    def set_bytes(i: Int, bytes: Option[Bytes]): Unit = set_bytes(i, bytes.orNull)
    3.59 +
    3.60 +    def set_date(i: Int, date: Date): Unit = db.set_date(stmt, i, date)
    3.61 +    def set_date(i: Int, date: Option[Date]): Unit = set_date(i, date.orNull)
    3.62 +
    3.63 +
    3.64 +    def execute(): Boolean = rep.execute()
    3.65 +    def execute_query(): Result = new Result(this, rep.executeQuery())
    3.66 +
    3.67 +    def close(): Unit = rep.close
    3.68 +  }
    3.69 +
    3.70 +
    3.71    /* results */
    3.72  
    3.73 -  def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
    3.74 +  class Result private[SQL](val stmt: Statement, val rep: ResultSet)
    3.75    {
    3.76 -    private var _next: Boolean = rs.next()
    3.77 -    def hasNext: Boolean = _next
    3.78 -    def next: A = { val x = get(rs); _next = rs.next(); x }
    3.79 +    res =>
    3.80 +
    3.81 +    def next(): Boolean = rep.next()
    3.82 +
    3.83 +    def iterator[A](get: Result => A): Iterator[A] = new Iterator[A]
    3.84 +    {
    3.85 +      private var _next: Boolean = res.next()
    3.86 +      def hasNext: Boolean = _next
    3.87 +      def next: A = { val x = get(res); _next = res.next(); x }
    3.88 +    }
    3.89 +
    3.90 +    def bool(column: Column): Boolean = rep.getBoolean(column.name)
    3.91 +    def int(column: Column): Int = rep.getInt(column.name)
    3.92 +    def long(column: Column): Long = rep.getLong(column.name)
    3.93 +    def double(column: Column): Double = rep.getDouble(column.name)
    3.94 +    def string(column: Column): String =
    3.95 +    {
    3.96 +      val s = rep.getString(column.name)
    3.97 +      if (s == null) "" else s
    3.98 +    }
    3.99 +    def bytes(column: Column): Bytes =
   3.100 +    {
   3.101 +      val bs = rep.getBytes(column.name)
   3.102 +      if (bs == null) Bytes.empty else Bytes(bs)
   3.103 +    }
   3.104 +    def date(column: Column): Date = stmt.db.date(res, column)
   3.105 +
   3.106 +    def get[A](column: Column, f: Column => A): Option[A] =
   3.107 +    {
   3.108 +      val x = f(column)
   3.109 +      if (rep.wasNull) None else Some(x)
   3.110 +    }
   3.111 +    def get_bool(column: Column): Option[Boolean] = get(column, bool _)
   3.112 +    def get_int(column: Column): Option[Int] = get(column, int _)
   3.113 +    def get_long(column: Column): Option[Long] = get(column, long _)
   3.114 +    def get_double(column: Column): Option[Double] = get(column, double _)
   3.115 +    def get_string(column: Column): Option[String] = get(column, string _)
   3.116 +    def get_bytes(column: Column): Option[Bytes] = get(column, bytes _)
   3.117 +    def get_date(column: Column): Option[Date] = get(column, date _)
   3.118    }
   3.119  
   3.120 +
   3.121 +  /* database */
   3.122 +
   3.123    trait Database
   3.124    {
   3.125 +    db =>
   3.126 +
   3.127 +
   3.128      /* types */
   3.129  
   3.130      def sql_type(T: Type.Value): Source
   3.131 @@ -205,100 +304,29 @@
   3.132      }
   3.133  
   3.134  
   3.135 -    /* statements */
   3.136 +    /* statements and results */
   3.137 +
   3.138 +    def statement(sql: Source): Statement =
   3.139 +      new Statement(db, connection.prepareStatement(sql))
   3.140  
   3.141 -    def statement(sql: Source): PreparedStatement =
   3.142 -      connection.prepareStatement(sql)
   3.143 +    def using_statement[A](sql: Source)(f: Statement => A): A =
   3.144 +      using(statement(sql))(f)
   3.145  
   3.146 -    def using_statement[A](sql: Source)(f: PreparedStatement => A): A =
   3.147 -      using(statement(sql))(f)
   3.148 +    def set_date(stmt: Statement, i: Int, date: Date): Unit
   3.149 +    def date(res: Result, column: Column): Date
   3.150  
   3.151      def insert_permissive(table: Table, sql: Source = ""): Source
   3.152  
   3.153  
   3.154 -    /* input */
   3.155 -
   3.156 -    def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) }
   3.157 -    def set_bool(stmt: PreparedStatement, i: Int, x: Option[Boolean])
   3.158 -    {
   3.159 -      if (x.isDefined) set_bool(stmt, i, x.get)
   3.160 -      else stmt.setNull(i, java.sql.Types.BOOLEAN)
   3.161 -    }
   3.162 -
   3.163 -    def set_int(stmt: PreparedStatement, i: Int, x: Int) { stmt.setInt(i, x) }
   3.164 -    def set_int(stmt: PreparedStatement, i: Int, x: Option[Int])
   3.165 -    {
   3.166 -      if (x.isDefined) set_int(stmt, i, x.get)
   3.167 -      else stmt.setNull(i, java.sql.Types.INTEGER)
   3.168 -    }
   3.169 -
   3.170 -    def set_long(stmt: PreparedStatement, i: Int, x: Long) { stmt.setLong(i, x) }
   3.171 -    def set_long(stmt: PreparedStatement, i: Int, x: Option[Long])
   3.172 -    {
   3.173 -      if (x.isDefined) set_long(stmt, i, x.get)
   3.174 -      else stmt.setNull(i, java.sql.Types.BIGINT)
   3.175 -    }
   3.176 -
   3.177 -    def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
   3.178 -    def set_double(stmt: PreparedStatement, i: Int, x: Option[Double])
   3.179 -    {
   3.180 -      if (x.isDefined) set_double(stmt, i, x.get)
   3.181 -      else stmt.setNull(i, java.sql.Types.DOUBLE)
   3.182 -    }
   3.183 -
   3.184 -    def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
   3.185 -    def set_string(stmt: PreparedStatement, i: Int, x: Option[String]): Unit =
   3.186 -      set_string(stmt, i, x.orNull)
   3.187 -
   3.188 -    def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
   3.189 -    {
   3.190 -      if (bytes == null) stmt.setBytes(i, null)
   3.191 -      else stmt.setBinaryStream(i, bytes.stream(), bytes.length)
   3.192 -    }
   3.193 -    def set_bytes(stmt: PreparedStatement, i: Int, bytes: Option[Bytes]): Unit =
   3.194 -      set_bytes(stmt, i, bytes.orNull)
   3.195 -
   3.196 -    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit
   3.197 -    def set_date(stmt: PreparedStatement, i: Int, date: Option[Date]): Unit =
   3.198 -      set_date(stmt, i, date.orNull)
   3.199 -
   3.200 -
   3.201 -    /* output */
   3.202 -
   3.203 -    def bool(rs: ResultSet, column: Column): Boolean = rs.getBoolean(column.name)
   3.204 -    def int(rs: ResultSet, column: Column): Int = rs.getInt(column.name)
   3.205 -    def long(rs: ResultSet, column: Column): Long = rs.getLong(column.name)
   3.206 -    def double(rs: ResultSet, column: Column): Double = rs.getDouble(column.name)
   3.207 -    def string(rs: ResultSet, column: Column): String =
   3.208 -    {
   3.209 -      val s = rs.getString(column.name)
   3.210 -      if (s == null) "" else s
   3.211 -    }
   3.212 -    def bytes(rs: ResultSet, column: Column): Bytes =
   3.213 -    {
   3.214 -      val bs = rs.getBytes(column.name)
   3.215 -      if (bs == null) Bytes.empty else Bytes(bs)
   3.216 -    }
   3.217 -    def date(rs: ResultSet, column: Column): Date
   3.218 -
   3.219 -    def get[A](rs: ResultSet, column: Column, f: (ResultSet, Column) => A): Option[A] =
   3.220 -    {
   3.221 -      val x = f(rs, column)
   3.222 -      if (rs.wasNull) None else Some(x)
   3.223 -    }
   3.224 -    def get_bool(rs: ResultSet, column: Column): Option[Boolean] = get(rs, column, bool _)
   3.225 -    def get_int(rs: ResultSet, column: Column): Option[Int] = get(rs, column, int _)
   3.226 -    def get_long(rs: ResultSet, column: Column): Option[Long] = get(rs, column, long _)
   3.227 -    def get_double(rs: ResultSet, column: Column): Option[Double] = get(rs, column, double _)
   3.228 -    def get_string(rs: ResultSet, column: Column): Option[String] = get(rs, column, string _)
   3.229 -    def get_bytes(rs: ResultSet, column: Column): Option[Bytes] = get(rs, column, bytes _)
   3.230 -    def get_date(rs: ResultSet, column: Column): Option[Date] = get(rs, column, date _)
   3.231 -
   3.232 -
   3.233      /* tables and views */
   3.234  
   3.235      def tables: List[String] =
   3.236 -      iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
   3.237 +    {
   3.238 +      val result = new mutable.ListBuffer[String]
   3.239 +      val rs = connection.getMetaData.getTables(null, null, "%", null)
   3.240 +      while (rs.next) { result += rs.getString(3) }
   3.241 +      result.toList
   3.242 +    }
   3.243  
   3.244      def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
   3.245        using_statement(
   3.246 @@ -345,12 +373,12 @@
   3.247  
   3.248      def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
   3.249  
   3.250 -    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
   3.251 -      if (date == null) set_string(stmt, i, null: String)
   3.252 -      else set_string(stmt, i, date_format(date))
   3.253 +    def set_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
   3.254 +      if (date == null) stmt.set_string(i, null: String)
   3.255 +      else stmt.set_string(i, date_format(date))
   3.256  
   3.257 -    def date(rs: ResultSet, column: SQL.Column): Date =
   3.258 -      date_format.parse(string(rs, column))
   3.259 +    def date(res: SQL.Result, column: SQL.Column): Date =
   3.260 +      date_format.parse(res.string(column))
   3.261  
   3.262      def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
   3.263        table.insert_cmd("INSERT OR IGNORE", sql = sql)
   3.264 @@ -418,13 +446,13 @@
   3.265      def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
   3.266  
   3.267      // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
   3.268 -    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
   3.269 -      if (date == null) stmt.setObject(i, null)
   3.270 -      else stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
   3.271 +    def set_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
   3.272 +      if (date == null) stmt.rep.setObject(i, null)
   3.273 +      else stmt.rep.setObject(i, OffsetDateTime.from(date.to_utc.rep))
   3.274  
   3.275 -    def date(rs: ResultSet, column: SQL.Column): Date =
   3.276 +    def date(res: SQL.Result, column: SQL.Column): Date =
   3.277      {
   3.278 -      val obj = rs.getObject(column.name, classOf[OffsetDateTime])
   3.279 +      val obj = res.rep.getObject(column.name, classOf[OffsetDateTime])
   3.280        if (obj == null) null else Date.instant(obj.toInstant)
   3.281      }
   3.282  
     4.1 --- a/src/Pure/Thy/sessions.scala	Sat May 06 11:43:43 2017 +0200
     4.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 06 12:45:42 2017 +0200
     4.3 @@ -10,7 +10,6 @@
     4.4  import java.nio.ByteBuffer
     4.5  import java.nio.channels.FileChannel
     4.6  import java.nio.file.StandardOpenOption
     4.7 -import java.sql.PreparedStatement
     4.8  
     4.9  import scala.collection.SortedSet
    4.10  import scala.collection.mutable
    4.11 @@ -766,8 +765,8 @@
    4.12        db.using_statement(Session_Info.table.select(List(column),
    4.13          Session_Info.session_name.where_equal(name)))(stmt =>
    4.14        {
    4.15 -        val rs = stmt.executeQuery
    4.16 -        if (!rs.next) Bytes.empty else db.bytes(rs, column)
    4.17 +        val res = stmt.execute_query()
    4.18 +        if (!res.next()) Bytes.empty else res.bytes(column)
    4.19        })
    4.20  
    4.21      def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    4.22 @@ -825,15 +824,15 @@
    4.23            Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    4.24          db.using_statement(Session_Info.table.insert())(stmt =>
    4.25          {
    4.26 -          db.set_string(stmt, 1, name)
    4.27 -          db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    4.28 -          db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
    4.29 -          db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
    4.30 -          db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
    4.31 -          db.set_string(stmt, 6, cat_lines(build.sources))
    4.32 -          db.set_string(stmt, 7, cat_lines(build.input_heaps))
    4.33 -          db.set_string(stmt, 8, build.output_heap getOrElse "")
    4.34 -          db.set_int(stmt, 9, build.return_code)
    4.35 +          stmt.set_string(1, name)
    4.36 +          stmt.set_bytes(2, encode_properties(build_log.session_timing))
    4.37 +          stmt.set_bytes(3, compress_properties(build_log.command_timings))
    4.38 +          stmt.set_bytes(4, compress_properties(build_log.ml_statistics))
    4.39 +          stmt.set_bytes(5, compress_properties(build_log.task_statistics))
    4.40 +          stmt.set_string(6, cat_lines(build.sources))
    4.41 +          stmt.set_string(7, cat_lines(build.input_heaps))
    4.42 +          stmt.set_string(8, build.output_heap getOrElse "")
    4.43 +          stmt.set_int(9, build.return_code)
    4.44            stmt.execute()
    4.45          })
    4.46        }
    4.47 @@ -867,15 +866,15 @@
    4.48        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    4.49          Session_Info.session_name.where_equal(name)))(stmt =>
    4.50        {
    4.51 -        val rs = stmt.executeQuery
    4.52 -        if (!rs.next) None
    4.53 +        val res = stmt.execute_query()
    4.54 +        if (!res.next()) None
    4.55          else {
    4.56            Some(
    4.57              Build.Session_Info(
    4.58 -              split_lines(db.string(rs, Session_Info.sources)),
    4.59 -              split_lines(db.string(rs, Session_Info.input_heaps)),
    4.60 -              db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
    4.61 -              db.int(rs, Session_Info.return_code)))
    4.62 +              split_lines(res.string(Session_Info.sources)),
    4.63 +              split_lines(res.string(Session_Info.input_heaps)),
    4.64 +              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    4.65 +              res.int(Session_Info.return_code)))
    4.66          }
    4.67        })
    4.68    }