# HG changeset patch # User wenzelm # Date 1494096743 -7200 # Node ID 1f4a80e80c8824e0244d2a91af55b17aa4bbaed8 # Parent 5a3052b2095f9d24e8bb353d75e7f66e84ecc15f tuned signature; diff -r 5a3052b2095f -r 1f4a80e80c88 src/Pure/Admin/build_log.scala --- 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() } }) diff -r 5a3052b2095f -r 1f4a80e80c88 src/Pure/General/sql.scala --- 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)) diff -r 5a3052b2095f -r 1f4a80e80c88 src/Pure/Thy/sessions.scala --- 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() }) }