--- a/src/Pure/Admin/build_log.scala Sat May 06 20:51:33 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Sat May 06 20:52:23 2017 +0200
@@ -803,8 +803,9 @@
{
val res = stmt.execute_query()
while (res.next()) {
- for ((c, i) <- table.columns.zipWithIndex)
- stmt2.set_string(i + 1, res.get_string(c))
+ for ((c, i) <- table.columns.zipWithIndex) {
+ stmt2.string(i + 1) = res.get_string(c)
+ }
stmt2.execute()
}
})
@@ -828,12 +829,12 @@
val table = Data.meta_info_table
db.using_statement(db.insert_permissive(table))(stmt =>
{
- stmt.set_string(1, log_name)
+ stmt.string(1) = log_name
for ((c, i) <- table.columns.tail.zipWithIndex) {
if (c.T == SQL.Type.Date)
- stmt.set_date(i + 2, meta_info.get_date(c))
+ stmt.date(i + 2) = meta_info.get_date(c)
else
- stmt.set_string(i + 2, meta_info.get(c))
+ stmt.string(i + 2) = meta_info.get(c)
}
stmt.execute()
})
@@ -848,21 +849,21 @@
if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
else build_info.sessions.iterator
for ((session_name, session) <- entries_iterator) {
- 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.string(1) = log_name
+ stmt.string(2) = session_name
+ stmt.string(3) = session.proper_chapter
+ stmt.string(4) = session.proper_groups
+ stmt.int(5) = session.threads
+ stmt.long(6) = session.timing.elapsed.proper_ms
+ stmt.long(7) = session.timing.cpu.proper_ms
+ stmt.long(8) = session.timing.gc.proper_ms
+ stmt.double(9) = session.timing.factor
+ stmt.long(10) = session.ml_timing.elapsed.proper_ms
+ stmt.long(11) = session.ml_timing.cpu.proper_ms
+ stmt.long(12) = session.ml_timing.gc.proper_ms
+ stmt.double(13) = session.ml_timing.factor
+ stmt.long(14) = session.heap_size
+ stmt.string(15) = session.status.map(_.toString)
stmt.execute()
}
})
@@ -879,9 +880,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) {
- stmt.set_string(1, log_name)
- stmt.set_string(2, session_name)
- stmt.set_bytes(3, ml_statistics)
+ stmt.string(1) = log_name
+ stmt.string(2) = session_name
+ stmt.bytes(3) = ml_statistics
stmt.execute()
}
})
--- a/src/Pure/General/sql.scala Sat May 06 20:51:33 2017 +0200
+++ b/src/Pure/General/sql.scala Sat May 06 20:52:23 2017 +0200
@@ -174,47 +174,61 @@
{
stmt =>
- def set_bool(i: Int, x: Boolean) { rep.setBoolean(i, x) }
- def set_bool(i: Int, x: Option[Boolean])
+ object bool
{
- if (x.isDefined) set_bool(i, x.get)
- else rep.setNull(i, java.sql.Types.BOOLEAN)
+ def update(i: Int, x: Boolean) { rep.setBoolean(i, x) }
+ def update(i: Int, x: Option[Boolean])
+ {
+ if (x.isDefined) update(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])
+ object int
{
- if (x.isDefined) set_int(i, x.get)
- else rep.setNull(i, java.sql.Types.INTEGER)
+ def update(i: Int, x: Int) { rep.setInt(i, x) }
+ def update(i: Int, x: Option[Int])
+ {
+ if (x.isDefined) update(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])
+ object long
{
- if (x.isDefined) set_long(i, x.get)
- else rep.setNull(i, java.sql.Types.BIGINT)
+ def update(i: Int, x: Long) { rep.setLong(i, x) }
+ def update(i: Int, x: Option[Long])
+ {
+ if (x.isDefined) update(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])
+ object double
{
- if (x.isDefined) set_double(i, x.get)
- else rep.setNull(i, java.sql.Types.DOUBLE)
+ def update(i: Int, x: Double) { rep.setDouble(i, x) }
+ def update(i: Int, x: Option[Double])
+ {
+ if (x.isDefined) update(i, x.get)
+ else rep.setNull(i, java.sql.Types.DOUBLE)
+ }
+ }
+ object string
+ {
+ def update(i: Int, x: String) { rep.setString(i, x) }
+ def update(i: Int, x: Option[String]): Unit = update(i, x.orNull)
}
-
- 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)
+ object bytes
{
- if (bytes == null) rep.setBytes(i, null)
- else rep.setBinaryStream(i, bytes.stream(), bytes.length)
+ def update(i: Int, bytes: Bytes)
+ {
+ if (bytes == null) rep.setBytes(i, null)
+ else rep.setBinaryStream(i, bytes.stream(), bytes.length)
+ }
+ def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull)
}
- 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)
-
+ object date
+ {
+ def update(i: Int, date: Date): Unit = db.update_date(stmt, i, date)
+ def update(i: Int, date: Option[Date]): Unit = update(i, date.orNull)
+ }
def execute(): Boolean = rep.execute()
def execute_query(): Result = new Result(this, rep.executeQuery())
@@ -315,7 +329,7 @@
def using_statement[A](sql: Source)(f: Statement => A): A =
using(statement(sql))(f)
- def set_date(stmt: Statement, i: Int, date: Date): Unit
+ def update_date(stmt: Statement, i: Int, date: Date): Unit
def date(res: Result, column: Column): Date
def insert_permissive(table: Table, sql: Source = ""): Source
@@ -376,9 +390,9 @@
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
- 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 update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
+ if (date == null) stmt.string(i) = (null: String)
+ else stmt.string(i) = date_format(date)
def date(res: SQL.Result, column: SQL.Column): Date =
date_format.parse(res.string(column))
@@ -449,7 +463,7 @@
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: SQL.Statement, i: Int, date: Date): Unit =
+ def update_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))
--- a/src/Pure/Thy/sessions.scala Sat May 06 20:51:33 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sat May 06 20:52:23 2017 +0200
@@ -824,15 +824,15 @@
Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
db.using_statement(Session_Info.table.insert())(stmt =>
{
- 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.string(1) = name
+ stmt.bytes(2) = encode_properties(build_log.session_timing)
+ stmt.bytes(3) = compress_properties(build_log.command_timings)
+ stmt.bytes(4) = compress_properties(build_log.ml_statistics)
+ stmt.bytes(5) = compress_properties(build_log.task_statistics)
+ stmt.string(6) = cat_lines(build.sources)
+ stmt.string(7) = cat_lines(build.input_heaps)
+ stmt.string(8) = build.output_heap getOrElse ""
+ stmt.int(9) = build.return_code
stmt.execute()
})
}