# HG changeset patch # User wenzelm # Date 1494067542 -7200 # Node ID 83388f09e9ab3bcd78d1c7f7fc6e8fea98efcc98 # Parent 3f206cfca625883bcc93166ec270422d2f1be67d clarified signature; diff -r 3f206cfca625 -r 83388f09e9ab src/Pure/Admin/build_log.scala --- 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 diff -r 3f206cfca625 -r 83388f09e9ab src/Pure/Admin/build_stats.scala --- 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) diff -r 3f206cfca625 -r 83388f09e9ab src/Pure/General/sql.scala --- 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) } diff -r 3f206cfca625 -r 83388f09e9ab src/Pure/Thy/sessions.scala --- 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))) } }) }