# HG changeset patch # User wenzelm # Date 1493373031 -7200 # Node ID d9533e9615ade1068a90ab1729fd1f68c4666304 # Parent e76d8f3e5478d4a5cbbe4d9e7216e5709411918e tuned signature; diff -r e76d8f3e5478 -r d9533e9615ad src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Fri Apr 28 11:45:44 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Fri Apr 28 11:50:31 2017 +0200 @@ -627,7 +627,7 @@ def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column]) : PreparedStatement = - db.select_statement(table, columns, log_filename.sql_where_eq_string(name)) + db.select_statement(table, columns, log_filename.sql_where_equal(name)) } def store(options: Options): Store = new Store(options) diff -r e76d8f3e5478 -r d9533e9615ad src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Fri Apr 28 11:45:44 2017 +0200 +++ b/src/Pure/General/sql.scala Fri Apr 28 11:50:31 2017 +0200 @@ -92,7 +92,7 @@ sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "") def sql_where_eq: String = "WHERE " + sql_name + " = " - def sql_where_eq_string(s: String): String = sql_where_eq + quote_string(s) + def sql_where_equal(s: String): String = sql_where_eq + quote_string(s) override def toString: String = sql_decl(sql_type_default) } diff -r e76d8f3e5478 -r d9533e9615ad src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Apr 28 11:45:44 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Apr 28 11:50:31 2017 +0200 @@ -750,10 +750,10 @@ def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column]) : PreparedStatement = - db.select_statement(table, columns, session_name.sql_where_eq_string(name)) + db.select_statement(table, columns, session_name.sql_where_equal(name)) def delete_statement(db: SQL.Database, name: String): PreparedStatement = - db.delete_statement(table, session_name.sql_where_eq_string(name)) + db.delete_statement(table, session_name.sql_where_equal(name)) } def store(system_mode: Boolean = false): Store = new Store(system_mode)