tuned signature;
authorwenzelm
Fri Apr 28 11:50:31 2017 +0200 (2017-04-28)
changeset 65602d9533e9615ad
parent 65601 e76d8f3e5478
child 65603 d6fe8a277576
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 11:45:44 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 11:50:31 2017 +0200
     1.3 @@ -627,7 +627,7 @@
     1.4  
     1.5      def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
     1.6          : PreparedStatement =
     1.7 -      db.select_statement(table, columns, log_filename.sql_where_eq_string(name))
     1.8 +      db.select_statement(table, columns, log_filename.sql_where_equal(name))
     1.9    }
    1.10  
    1.11    def store(options: Options): Store = new Store(options)
     2.1 --- a/src/Pure/General/sql.scala	Fri Apr 28 11:45:44 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Fri Apr 28 11:50:31 2017 +0200
     2.3 @@ -92,7 +92,7 @@
     2.4        sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
     2.5  
     2.6      def sql_where_eq: String = "WHERE " + sql_name + " = "
     2.7 -    def sql_where_eq_string(s: String): String = sql_where_eq + quote_string(s)
     2.8 +    def sql_where_equal(s: String): String = sql_where_eq + quote_string(s)
     2.9  
    2.10      override def toString: String = sql_decl(sql_type_default)
    2.11    }
     3.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 28 11:45:44 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 11:50:31 2017 +0200
     3.3 @@ -750,10 +750,10 @@
     3.4  
     3.5      def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
     3.6          : PreparedStatement =
     3.7 -      db.select_statement(table, columns, session_name.sql_where_eq_string(name))
     3.8 +      db.select_statement(table, columns, session_name.sql_where_equal(name))
     3.9  
    3.10      def delete_statement(db: SQL.Database, name: String): PreparedStatement =
    3.11 -      db.delete_statement(table, session_name.sql_where_eq_string(name))
    3.12 +      db.delete_statement(table, session_name.sql_where_equal(name))
    3.13    }
    3.14  
    3.15    def store(system_mode: Boolean = false): Store = new Store(system_mode)