# HG changeset patch
# User wenzelm
# Date 1493819603 -7200
# Node ID 9f74d9aa0bdfc3f4ac116337137f7c85a2ff32c8
# Parent  38139b2067cfecae05cc15d35cee11ffc0a3001b
tuned signature;

diff -r 38139b2067cf -r 9f74d9aa0bdf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 03 15:51:34 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:53:23 2017 +0200
@@ -789,7 +789,7 @@
       val table = Data.meta_info_table
 
       db.transaction {
-        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
         db.using_statement(table.insert())(stmt =>
         {
           db.set_string(stmt, 1, log_file.name)
@@ -810,7 +810,7 @@
       val table = Data.sessions_table
 
       db.transaction {
-        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
         db.using_statement(table.insert())(stmt =>
         {
           val entries_iterator =
@@ -844,7 +844,7 @@
       val table = Data.ml_statistics_table
 
       db.transaction {
-        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
+        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
         db.using_statement(table.insert())(stmt =>
         {
           val ml_stats: List[(String, Option[Bytes])] =
@@ -896,7 +896,7 @@
     {
       val table = Data.meta_info_table
       val columns = table.columns.tail
-      db.using_statement(table.select(columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
+      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None
@@ -925,7 +925,7 @@
       val table2 = Data.ml_statistics_table
 
       val where_log_name =
-        Data.log_name(table1).sql_where_equal(log_name) + " AND " +
+        Data.log_name(table1).where_equal(log_name) + " AND " +
           Data.session_name(table1).ident + " <> ''"
       val where =
         if (session_names.isEmpty) where_log_name
diff -r 38139b2067cf -r 9f74d9aa0bdf src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed May 03 15:51:34 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 15:53:23 2017 +0200
@@ -106,8 +106,7 @@
     def sql_decl(sql_type: Type.Value => String): String =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
-    def sql_where_eq: String = "WHERE " + ident + " = "
-    def sql_where_equal(s: String): String = sql_where_eq + string(s)
+    def where_equal(s: String): String = "WHERE " + ident + " = " + string(s)
 
     override def toString: String = sql_decl(sql_type_default)
   }
diff -r 38139b2067cf -r 9f74d9aa0bdf src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed May 03 15:51:34 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed May 03 15:53:23 2017 +0200
@@ -764,7 +764,7 @@
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
       db.using_statement(Session_Info.table.select(List(column),
-        Session_Info.session_name.sql_where_equal(name)))(stmt =>
+        Session_Info.session_name.where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) Bytes.empty else db.bytes(rs, column)
@@ -822,7 +822,7 @@
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
-          Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
+          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)
@@ -865,7 +865,7 @@
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
       db.using_statement(Session_Info.table.select(Session_Info.build_columns,
-        Session_Info.session_name.sql_where_equal(name)))(stmt =>
+        Session_Info.session_name.where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None