--- 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