# HG changeset patch
# User wenzelm
# Date 1493402614 -7200
# Node ID e33b3d57b7cb9f3820441964d155e6471058fd20
# Parent  986fac3c60b4007f35774e33fb9ca398d9c21567
tuned signature;

diff -r 986fac3c60b4 -r e33b3d57b7cb src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 18:52:31 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 20:03:34 2017 +0200
@@ -649,7 +649,7 @@
 
         val key = Meta_Info.log_name
         val known_files =
-          using(db.select_statement(table, List(key)))(stmt =>
+          using(db.select(table, List(key)))(stmt =>
             SQL.iterator(stmt.executeQuery)(rs => db.string(rs, key)).toSet)
 
         val unique_files =
@@ -670,9 +670,9 @@
             val log_file = Log_File(file)
             val meta_info = log_file.parse_meta_info()
 
-            using(db.delete_statement(
-              Meta_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
-            using(db.insert_statement(Meta_Info.table))(stmt =>
+            using(db.delete(Meta_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(
+              _.execute)
+            using(db.insert(Meta_Info.table))(stmt =>
             {
               db.set_string(stmt, 1, log_file.name)
               for ((c, i) <- Meta_Info.table.columns.tail.zipWithIndex) {
@@ -696,9 +696,9 @@
             val log_file = Log_File(file)
             val build_info = log_file.parse_build_info()
 
-            using(db.delete_statement(
-              Build_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
-            using(db.insert_statement(Build_Info.table))(stmt =>
+            using(db.delete(Build_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(
+              _.execute)
+            using(db.insert(Build_Info.table))(stmt =>
             {
               for ((session_name, session) <- build_info.sessions.iterator) {
                 db.set_string(stmt, 1, log_file.name)
diff -r 986fac3c60b4 -r e33b3d57b7cb src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Apr 28 18:52:31 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri Apr 28 20:03:34 2017 +0200
@@ -198,13 +198,13 @@
 
     def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
 
-    def insert_statement(table: Table): PreparedStatement = statement(table.sql_insert)
+    def insert(table: Table): PreparedStatement = statement(table.sql_insert)
 
-    def delete_statement(table: Table, sql: String = ""): PreparedStatement =
+    def delete(table: Table, sql: String = ""): PreparedStatement =
       statement(table.sql_delete + (if (sql == "") "" else " " + sql))
 
-    def select_statement(table: Table, columns: List[Column],
-        sql: String = "", distinct: Boolean = false): PreparedStatement =
+    def select(table: Table, columns: List[Column], sql: String = "", distinct: Boolean = false)
+        : PreparedStatement =
       statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
 
 
diff -r 986fac3c60b4 -r e33b3d57b7cb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 28 18:52:31 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 20:03:34 2017 +0200
@@ -763,7 +763,7 @@
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
-      using(db.select_statement(Session_Info.table, List(column),
+      using(db.select(Session_Info.table, List(column),
         Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
@@ -821,9 +821,9 @@
     {
       db.transaction {
         db.create_table(Session_Info.table)
-        using(db.delete_statement(Session_Info.table,
-          Session_Info.session_name.sql_where_equal(name)))(_.execute)
-        using(db.insert_statement(Session_Info.table))(stmt =>
+        using(db.delete(Session_Info.table, Session_Info.session_name.sql_where_equal(name)))(
+          _.execute)
+        using(db.insert(Session_Info.table))(stmt =>
         {
           db.set_string(stmt, 1, name)
           db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
@@ -864,7 +864,7 @@
     }
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
-      using(db.select_statement(Session_Info.table, Session_Info.build_columns,
+      using(db.select(Session_Info.table, Session_Info.build_columns,
         Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery