--- a/src/Pure/Admin/build_log.scala Sat May 06 11:43:43 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Sat May 06 12:45:42 2017 +0200
@@ -11,7 +11,6 @@
import java.time.ZoneId
import java.time.format.{DateTimeFormatter, DateTimeParseException}
import java.util.Locale
-import java.sql.PreparedStatement
import scala.collection.immutable.SortedMap
import scala.collection.mutable
@@ -781,8 +780,8 @@
val recent_log_names =
db.using_statement(
Data.select_recent(
- Data.meta_info_table, List(Data.log_name), days, distinct = true))(
- stmt => SQL.iterator(stmt.executeQuery)(db.string(_, Data.log_name)).toList)
+ Data.meta_info_table, List(Data.log_name), days, distinct = true))(stmt =>
+ stmt.execute_query().iterator(_.string(Data.log_name)).toList)
for (log_name <- recent_log_names) {
read_meta_info(db, log_name).foreach(meta_info =>
@@ -802,11 +801,11 @@
{
db.using_statement(Data.recent_table(days).query)(stmt =>
{
- val rs = stmt.executeQuery
- while (rs.next()) {
+ val res = stmt.execute_query()
+ while (res.next()) {
for ((c, i) <- table.columns.zipWithIndex)
- db2.set_string(stmt2, i + 1, db.get_string(rs, c))
- stmt2.execute
+ stmt2.set_string(i + 1, res.get_string(c))
+ stmt2.execute()
}
})
})
@@ -822,19 +821,19 @@
def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
db.using_statement(table.select(List(column), distinct = true))(stmt =>
- SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
+ stmt.execute_query().iterator(_.string(column)).toSet)
def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
{
val table = Data.meta_info_table
db.using_statement(db.insert_permissive(table))(stmt =>
{
- db.set_string(stmt, 1, log_name)
+ stmt.set_string(1, log_name)
for ((c, i) <- table.columns.tail.zipWithIndex) {
if (c.T == SQL.Type.Date)
- db.set_date(stmt, i + 2, meta_info.get_date(c))
+ stmt.set_date(i + 2, meta_info.get_date(c))
else
- db.set_string(stmt, i + 2, meta_info.get(c))
+ stmt.set_string(i + 2, meta_info.get(c))
}
stmt.execute()
})
@@ -849,21 +848,21 @@
if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
else build_info.sessions.iterator
for ((session_name, session) <- entries_iterator) {
- db.set_string(stmt, 1, log_name)
- db.set_string(stmt, 2, session_name)
- db.set_string(stmt, 3, session.proper_chapter)
- db.set_string(stmt, 4, session.proper_groups)
- db.set_int(stmt, 5, session.threads)
- db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
- db.set_long(stmt, 7, session.timing.cpu.proper_ms)
- db.set_long(stmt, 8, session.timing.gc.proper_ms)
- db.set_double(stmt, 9, session.timing.factor)
- db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
- db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
- db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
- db.set_double(stmt, 13, session.ml_timing.factor)
- db.set_long(stmt, 14, session.heap_size)
- db.set_string(stmt, 15, session.status.map(_.toString))
+ stmt.set_string(1, log_name)
+ stmt.set_string(2, session_name)
+ stmt.set_string(3, session.proper_chapter)
+ stmt.set_string(4, session.proper_groups)
+ stmt.set_int(5, session.threads)
+ stmt.set_long(6, session.timing.elapsed.proper_ms)
+ stmt.set_long(7, session.timing.cpu.proper_ms)
+ stmt.set_long(8, session.timing.gc.proper_ms)
+ stmt.set_double(9, session.timing.factor)
+ stmt.set_long(10, session.ml_timing.elapsed.proper_ms)
+ stmt.set_long(11, session.ml_timing.cpu.proper_ms)
+ stmt.set_long(12, session.ml_timing.gc.proper_ms)
+ stmt.set_double(13, session.ml_timing.factor)
+ stmt.set_long(14, session.heap_size)
+ stmt.set_string(15, session.status.map(_.toString))
stmt.execute()
}
})
@@ -880,9 +879,9 @@
build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
for ((session_name, ml_statistics) <- entries) {
- db.set_string(stmt, 1, log_name)
- db.set_string(stmt, 2, session_name)
- db.set_bytes(stmt, 3, ml_statistics)
+ stmt.set_string(1, log_name)
+ stmt.set_string(2, session_name)
+ stmt.set_bytes(3, ml_statistics)
stmt.execute()
}
})
@@ -936,15 +935,15 @@
val columns = table.columns.tail
db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
{
- val rs = stmt.executeQuery
- if (!rs.next) None
+ val res = stmt.execute_query()
+ if (!res.next) None
else {
val results =
columns.map(c => c.name ->
(if (c.T == SQL.Type.Date)
- db.get_date(rs, c).map(Log_File.Date_Format(_))
+ res.get_date(c).map(Log_File.Date_Format(_))
else
- db.get_string(rs, c)))
+ res.get_string(c)))
val n = Prop.all_props.length
val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
@@ -987,26 +986,28 @@
val sessions =
db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
{
- SQL.iterator(stmt.executeQuery)(rs =>
+ stmt.execute_query().iterator(res =>
{
- val session_name = db.string(rs, Data.session_name)
+ val session_name = res.string(Data.session_name)
val session_entry =
Session_Entry(
- chapter = db.string(rs, Data.chapter),
- groups = split_lines(db.string(rs, Data.groups)),
- threads = db.get_int(rs, Data.threads),
+ chapter = res.string(Data.chapter),
+ groups = split_lines(res.string(Data.groups)),
+ threads = res.get_int(Data.threads),
timing =
- Timing(Time.ms(db.long(rs, Data.timing_elapsed)),
- Time.ms(db.long(rs, Data.timing_cpu)),
- Time.ms(db.long(rs, Data.timing_gc))),
+ Timing(
+ Time.ms(res.long(Data.timing_elapsed)),
+ Time.ms(res.long(Data.timing_cpu)),
+ Time.ms(res.long(Data.timing_gc))),
ml_timing =
- Timing(Time.ms(db.long(rs, Data.ml_timing_elapsed)),
- Time.ms(db.long(rs, Data.ml_timing_cpu)),
- Time.ms(db.long(rs, Data.ml_timing_gc))),
- heap_size = db.get_long(rs, Data.heap_size),
- status = db.get_string(rs, Data.status).map(Session_Status.withName(_)),
+ Timing(
+ Time.ms(res.long(Data.ml_timing_elapsed)),
+ Time.ms(res.long(Data.ml_timing_cpu)),
+ Time.ms(res.long(Data.ml_timing_gc))),
+ heap_size = res.get_long(Data.heap_size),
+ status = res.get_string(Data.status).map(Session_Status.withName(_)),
ml_statistics =
- if (ml_statistics) uncompress_properties(db.bytes(rs, Data.ml_statistics))
+ if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics))
else Nil)
session_name -> session_entry
}).toMap
--- a/src/Pure/Admin/build_stats.scala Sat May 06 11:43:43 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala Sat May 06 12:45:42 2017 +0200
@@ -79,26 +79,26 @@
db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
{
- val rs = stmt.executeQuery
- while (rs.next) {
- val ml_platform = db.string(rs, Build_Log.Settings.ML_PLATFORM)
- val threads = db.get_int(rs, Build_Log.Data.threads)
+ val res = stmt.execute_query()
+ while (res.next()) {
+ val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
+ val threads = res.get_int(Build_Log.Data.threads)
val name =
profile.name +
"_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
"_M" + threads.getOrElse(1)
- val session = db.string(rs, Build_Log.Data.session_name)
+ val session = res.string(Build_Log.Data.session_name)
val entry =
- Entry(db.date(rs, Build_Log.Data.pull_date),
+ Entry(res.date(Build_Log.Data.pull_date),
Timing(
- Time.ms(db.long(rs, Build_Log.Data.timing_elapsed)),
- Time.ms(db.long(rs, Build_Log.Data.timing_cpu)),
- Time.ms(db.long(rs, Build_Log.Data.timing_gc))),
+ Time.ms(res.long(Build_Log.Data.timing_elapsed)),
+ Time.ms(res.long(Build_Log.Data.timing_cpu)),
+ Time.ms(res.long(Build_Log.Data.timing_gc))),
Timing(
- Time.ms(db.long(rs, Build_Log.Data.ml_timing_elapsed)),
- Time.ms(db.long(rs, Build_Log.Data.ml_timing_cpu)),
- Time.ms(db.long(rs, Build_Log.Data.ml_timing_gc))))
+ Time.ms(res.long(Build_Log.Data.ml_timing_elapsed)),
+ Time.ms(res.long(Build_Log.Data.ml_timing_cpu)),
+ Time.ms(res.long(Build_Log.Data.ml_timing_gc))))
val session_entries = data.getOrElse(name, Map.empty)
val entries = session_entries.getOrElse(session, Nil)
--- a/src/Pure/General/sql.scala Sat May 06 11:43:43 2017 +0200
+++ b/src/Pure/General/sql.scala Sat May 06 12:45:42 2017 +0200
@@ -9,6 +9,8 @@
import java.time.OffsetDateTime
import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
+import scala.collection.mutable
+
object SQL
{
@@ -166,17 +168,114 @@
/** SQL database operations **/
+ /* statements */
+
+ class Statement private[SQL](val db: Database, val rep: PreparedStatement)
+ {
+ stmt =>
+
+ def set_bool(i: Int, x: Boolean) { rep.setBoolean(i, x) }
+ def set_bool(i: Int, x: Option[Boolean])
+ {
+ if (x.isDefined) set_bool(i, x.get)
+ else rep.setNull(i, java.sql.Types.BOOLEAN)
+ }
+
+ def set_int(i: Int, x: Int) { rep.setInt(i, x) }
+ def set_int(i: Int, x: Option[Int])
+ {
+ if (x.isDefined) set_int(i, x.get)
+ else rep.setNull(i, java.sql.Types.INTEGER)
+ }
+
+ def set_long(i: Int, x: Long) { rep.setLong(i, x) }
+ def set_long(i: Int, x: Option[Long])
+ {
+ if (x.isDefined) set_long(i, x.get)
+ else rep.setNull(i, java.sql.Types.BIGINT)
+ }
+
+ def set_double(i: Int, x: Double) { rep.setDouble(i, x) }
+ def set_double(i: Int, x: Option[Double])
+ {
+ if (x.isDefined) set_double(i, x.get)
+ else rep.setNull(i, java.sql.Types.DOUBLE)
+ }
+
+ def set_string(i: Int, x: String) { rep.setString(i, x) }
+ def set_string(i: Int, x: Option[String]): Unit = set_string(i, x.orNull)
+
+ def set_bytes(i: Int, bytes: Bytes)
+ {
+ if (bytes == null) rep.setBytes(i, null)
+ else rep.setBinaryStream(i, bytes.stream(), bytes.length)
+ }
+ def set_bytes(i: Int, bytes: Option[Bytes]): Unit = set_bytes(i, bytes.orNull)
+
+ def set_date(i: Int, date: Date): Unit = db.set_date(stmt, i, date)
+ def set_date(i: Int, date: Option[Date]): Unit = set_date(i, date.orNull)
+
+
+ def execute(): Boolean = rep.execute()
+ def execute_query(): Result = new Result(this, rep.executeQuery())
+
+ def close(): Unit = rep.close
+ }
+
+
/* results */
- def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
+ class Result private[SQL](val stmt: Statement, val rep: ResultSet)
{
- private var _next: Boolean = rs.next()
- def hasNext: Boolean = _next
- def next: A = { val x = get(rs); _next = rs.next(); x }
+ res =>
+
+ def next(): Boolean = rep.next()
+
+ def iterator[A](get: Result => A): Iterator[A] = new Iterator[A]
+ {
+ private var _next: Boolean = res.next()
+ def hasNext: Boolean = _next
+ def next: A = { val x = get(res); _next = res.next(); x }
+ }
+
+ def bool(column: Column): Boolean = rep.getBoolean(column.name)
+ def int(column: Column): Int = rep.getInt(column.name)
+ def long(column: Column): Long = rep.getLong(column.name)
+ def double(column: Column): Double = rep.getDouble(column.name)
+ def string(column: Column): String =
+ {
+ val s = rep.getString(column.name)
+ if (s == null) "" else s
+ }
+ def bytes(column: Column): Bytes =
+ {
+ val bs = rep.getBytes(column.name)
+ if (bs == null) Bytes.empty else Bytes(bs)
+ }
+ def date(column: Column): Date = stmt.db.date(res, column)
+
+ def get[A](column: Column, f: Column => A): Option[A] =
+ {
+ val x = f(column)
+ if (rep.wasNull) None else Some(x)
+ }
+ def get_bool(column: Column): Option[Boolean] = get(column, bool _)
+ def get_int(column: Column): Option[Int] = get(column, int _)
+ def get_long(column: Column): Option[Long] = get(column, long _)
+ def get_double(column: Column): Option[Double] = get(column, double _)
+ def get_string(column: Column): Option[String] = get(column, string _)
+ def get_bytes(column: Column): Option[Bytes] = get(column, bytes _)
+ def get_date(column: Column): Option[Date] = get(column, date _)
}
+
+ /* database */
+
trait Database
{
+ db =>
+
+
/* types */
def sql_type(T: Type.Value): Source
@@ -205,100 +304,29 @@
}
- /* statements */
+ /* statements and results */
+
+ def statement(sql: Source): Statement =
+ new Statement(db, connection.prepareStatement(sql))
- def statement(sql: Source): PreparedStatement =
- connection.prepareStatement(sql)
+ def using_statement[A](sql: Source)(f: Statement => A): A =
+ using(statement(sql))(f)
- def using_statement[A](sql: Source)(f: PreparedStatement => A): A =
- using(statement(sql))(f)
+ def set_date(stmt: Statement, i: Int, date: Date): Unit
+ def date(res: Result, column: Column): Date
def insert_permissive(table: Table, sql: Source = ""): Source
- /* input */
-
- def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) }
- def set_bool(stmt: PreparedStatement, i: Int, x: Option[Boolean])
- {
- if (x.isDefined) set_bool(stmt, i, x.get)
- else stmt.setNull(i, java.sql.Types.BOOLEAN)
- }
-
- def set_int(stmt: PreparedStatement, i: Int, x: Int) { stmt.setInt(i, x) }
- def set_int(stmt: PreparedStatement, i: Int, x: Option[Int])
- {
- if (x.isDefined) set_int(stmt, i, x.get)
- else stmt.setNull(i, java.sql.Types.INTEGER)
- }
-
- def set_long(stmt: PreparedStatement, i: Int, x: Long) { stmt.setLong(i, x) }
- def set_long(stmt: PreparedStatement, i: Int, x: Option[Long])
- {
- if (x.isDefined) set_long(stmt, i, x.get)
- else stmt.setNull(i, java.sql.Types.BIGINT)
- }
-
- def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
- def set_double(stmt: PreparedStatement, i: Int, x: Option[Double])
- {
- if (x.isDefined) set_double(stmt, i, x.get)
- else stmt.setNull(i, java.sql.Types.DOUBLE)
- }
-
- def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
- def set_string(stmt: PreparedStatement, i: Int, x: Option[String]): Unit =
- set_string(stmt, i, x.orNull)
-
- def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
- {
- if (bytes == null) stmt.setBytes(i, null)
- else stmt.setBinaryStream(i, bytes.stream(), bytes.length)
- }
- def set_bytes(stmt: PreparedStatement, i: Int, bytes: Option[Bytes]): Unit =
- set_bytes(stmt, i, bytes.orNull)
-
- def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit
- def set_date(stmt: PreparedStatement, i: Int, date: Option[Date]): Unit =
- set_date(stmt, i, date.orNull)
-
-
- /* output */
-
- def bool(rs: ResultSet, column: Column): Boolean = rs.getBoolean(column.name)
- def int(rs: ResultSet, column: Column): Int = rs.getInt(column.name)
- def long(rs: ResultSet, column: Column): Long = rs.getLong(column.name)
- def double(rs: ResultSet, column: Column): Double = rs.getDouble(column.name)
- def string(rs: ResultSet, column: Column): String =
- {
- val s = rs.getString(column.name)
- if (s == null) "" else s
- }
- def bytes(rs: ResultSet, column: Column): Bytes =
- {
- val bs = rs.getBytes(column.name)
- if (bs == null) Bytes.empty else Bytes(bs)
- }
- def date(rs: ResultSet, column: Column): Date
-
- def get[A](rs: ResultSet, column: Column, f: (ResultSet, Column) => A): Option[A] =
- {
- val x = f(rs, column)
- if (rs.wasNull) None else Some(x)
- }
- def get_bool(rs: ResultSet, column: Column): Option[Boolean] = get(rs, column, bool _)
- def get_int(rs: ResultSet, column: Column): Option[Int] = get(rs, column, int _)
- def get_long(rs: ResultSet, column: Column): Option[Long] = get(rs, column, long _)
- def get_double(rs: ResultSet, column: Column): Option[Double] = get(rs, column, double _)
- def get_string(rs: ResultSet, column: Column): Option[String] = get(rs, column, string _)
- def get_bytes(rs: ResultSet, column: Column): Option[Bytes] = get(rs, column, bytes _)
- def get_date(rs: ResultSet, column: Column): Option[Date] = get(rs, column, date _)
-
-
/* tables and views */
def tables: List[String] =
- iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
+ {
+ val result = new mutable.ListBuffer[String]
+ val rs = connection.getMetaData.getTables(null, null, "%", null)
+ while (rs.next) { result += rs.getString(3) }
+ result.toList
+ }
def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
using_statement(
@@ -345,12 +373,12 @@
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
- def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
- if (date == null) set_string(stmt, i, null: String)
- else set_string(stmt, i, date_format(date))
+ def set_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
+ if (date == null) stmt.set_string(i, null: String)
+ else stmt.set_string(i, date_format(date))
- def date(rs: ResultSet, column: SQL.Column): Date =
- date_format.parse(string(rs, column))
+ def date(res: SQL.Result, column: SQL.Column): Date =
+ date_format.parse(res.string(column))
def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
table.insert_cmd("INSERT OR IGNORE", sql = sql)
@@ -418,13 +446,13 @@
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
// see https://jdbc.postgresql.org/documentation/head/8-date-time.html
- def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
- if (date == null) stmt.setObject(i, null)
- else stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
+ def set_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
+ if (date == null) stmt.rep.setObject(i, null)
+ else stmt.rep.setObject(i, OffsetDateTime.from(date.to_utc.rep))
- def date(rs: ResultSet, column: SQL.Column): Date =
+ def date(res: SQL.Result, column: SQL.Column): Date =
{
- val obj = rs.getObject(column.name, classOf[OffsetDateTime])
+ val obj = res.rep.getObject(column.name, classOf[OffsetDateTime])
if (obj == null) null else Date.instant(obj.toInstant)
}
--- a/src/Pure/Thy/sessions.scala Sat May 06 11:43:43 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sat May 06 12:45:42 2017 +0200
@@ -10,7 +10,6 @@
import java.nio.ByteBuffer
import java.nio.channels.FileChannel
import java.nio.file.StandardOpenOption
-import java.sql.PreparedStatement
import scala.collection.SortedSet
import scala.collection.mutable
@@ -766,8 +765,8 @@
db.using_statement(Session_Info.table.select(List(column),
Session_Info.session_name.where_equal(name)))(stmt =>
{
- val rs = stmt.executeQuery
- if (!rs.next) Bytes.empty else db.bytes(rs, column)
+ val res = stmt.execute_query()
+ if (!res.next()) Bytes.empty else res.bytes(column)
})
def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
@@ -825,15 +824,15 @@
Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
db.using_statement(Session_Info.table.insert())(stmt =>
{
- db.set_string(stmt, 1, name)
- db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
- db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
- db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
- db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
- db.set_string(stmt, 6, cat_lines(build.sources))
- db.set_string(stmt, 7, cat_lines(build.input_heaps))
- db.set_string(stmt, 8, build.output_heap getOrElse "")
- db.set_int(stmt, 9, build.return_code)
+ stmt.set_string(1, name)
+ stmt.set_bytes(2, encode_properties(build_log.session_timing))
+ stmt.set_bytes(3, compress_properties(build_log.command_timings))
+ stmt.set_bytes(4, compress_properties(build_log.ml_statistics))
+ stmt.set_bytes(5, compress_properties(build_log.task_statistics))
+ stmt.set_string(6, cat_lines(build.sources))
+ stmt.set_string(7, cat_lines(build.input_heaps))
+ stmt.set_string(8, build.output_heap getOrElse "")
+ stmt.set_int(9, build.return_code)
stmt.execute()
})
}
@@ -867,15 +866,15 @@
db.using_statement(Session_Info.table.select(Session_Info.build_columns,
Session_Info.session_name.where_equal(name)))(stmt =>
{
- val rs = stmt.executeQuery
- if (!rs.next) None
+ val res = stmt.execute_query()
+ if (!res.next()) None
else {
Some(
Build.Session_Info(
- split_lines(db.string(rs, Session_Info.sources)),
- split_lines(db.string(rs, Session_Info.input_heaps)),
- db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
- db.int(rs, Session_Info.return_code)))
+ split_lines(res.string(Session_Info.sources)),
+ split_lines(res.string(Session_Info.input_heaps)),
+ res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+ res.int(Session_Info.return_code)))
}
})
}