tuned signature;
authorwenzelm
Fri Apr 28 20:03:34 2017 +0200 (2017-04-28)
changeset 65619e33b3d57b7cb
parent 65618 986fac3c60b4
child 65620 9b99d61be5af
tuned signature;
src/Pure/Admin/build_log.scala
src/Pure/General/sql.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Fri Apr 28 18:52:31 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 20:03:34 2017 +0200
     1.3 @@ -649,7 +649,7 @@
     1.4  
     1.5          val key = Meta_Info.log_name
     1.6          val known_files =
     1.7 -          using(db.select_statement(table, List(key)))(stmt =>
     1.8 +          using(db.select(table, List(key)))(stmt =>
     1.9              SQL.iterator(stmt.executeQuery)(rs => db.string(rs, key)).toSet)
    1.10  
    1.11          val unique_files =
    1.12 @@ -670,9 +670,9 @@
    1.13              val log_file = Log_File(file)
    1.14              val meta_info = log_file.parse_meta_info()
    1.15  
    1.16 -            using(db.delete_statement(
    1.17 -              Meta_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.18 -            using(db.insert_statement(Meta_Info.table))(stmt =>
    1.19 +            using(db.delete(Meta_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(
    1.20 +              _.execute)
    1.21 +            using(db.insert(Meta_Info.table))(stmt =>
    1.22              {
    1.23                db.set_string(stmt, 1, log_file.name)
    1.24                for ((c, i) <- Meta_Info.table.columns.tail.zipWithIndex) {
    1.25 @@ -696,9 +696,9 @@
    1.26              val log_file = Log_File(file)
    1.27              val build_info = log_file.parse_build_info()
    1.28  
    1.29 -            using(db.delete_statement(
    1.30 -              Build_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.31 -            using(db.insert_statement(Build_Info.table))(stmt =>
    1.32 +            using(db.delete(Build_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(
    1.33 +              _.execute)
    1.34 +            using(db.insert(Build_Info.table))(stmt =>
    1.35              {
    1.36                for ((session_name, session) <- build_info.sessions.iterator) {
    1.37                  db.set_string(stmt, 1, log_file.name)
     2.1 --- a/src/Pure/General/sql.scala	Fri Apr 28 18:52:31 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Fri Apr 28 20:03:34 2017 +0200
     2.3 @@ -198,13 +198,13 @@
     2.4  
     2.5      def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
     2.6  
     2.7 -    def insert_statement(table: Table): PreparedStatement = statement(table.sql_insert)
     2.8 +    def insert(table: Table): PreparedStatement = statement(table.sql_insert)
     2.9  
    2.10 -    def delete_statement(table: Table, sql: String = ""): PreparedStatement =
    2.11 +    def delete(table: Table, sql: String = ""): PreparedStatement =
    2.12        statement(table.sql_delete + (if (sql == "") "" else " " + sql))
    2.13  
    2.14 -    def select_statement(table: Table, columns: List[Column],
    2.15 -        sql: String = "", distinct: Boolean = false): PreparedStatement =
    2.16 +    def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
    2.17 +        : PreparedStatement =
    2.18        statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
    2.19  
    2.20  
     3.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 28 18:52:31 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 20:03:34 2017 +0200
     3.3 @@ -763,7 +763,7 @@
     3.4      /* SQL database content */
     3.5  
     3.6      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
     3.7 -      using(db.select_statement(Session_Info.table, List(column),
     3.8 +      using(db.select(Session_Info.table, List(column),
     3.9          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    3.10        {
    3.11          val rs = stmt.executeQuery
    3.12 @@ -821,9 +821,9 @@
    3.13      {
    3.14        db.transaction {
    3.15          db.create_table(Session_Info.table)
    3.16 -        using(db.delete_statement(Session_Info.table,
    3.17 -          Session_Info.session_name.sql_where_equal(name)))(_.execute)
    3.18 -        using(db.insert_statement(Session_Info.table))(stmt =>
    3.19 +        using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
    3.20 +          _.execute)
    3.21 +        using(db.insert(Session_Info.table))(stmt =>
    3.22          {
    3.23            db.set_string(stmt, 1, name)
    3.24            db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    3.25 @@ -864,7 +864,7 @@
    3.26      }
    3.27  
    3.28      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    3.29 -      using(db.select_statement(Session_Info.table, Session_Info.build_columns,
    3.30 +      using(db.select(Session_Info.table, Session_Info.build_columns,
    3.31          Session_Info.session_name.sql_where_equal(name)))(stmt =>
    3.32        {
    3.33          val rs = stmt.executeQuery