tuned signature;
authorwenzelm
Wed May 03 15:53:23 2017 +0200 (2017-05-03)
changeset 656999f74d9aa0bdf
parent 65698 38139b2067cf
child 65700 333961e15062
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	Wed May 03 15:51:34 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Wed May 03 15:53:23 2017 +0200
     1.3 @@ -789,7 +789,7 @@
     1.4        val table = Data.meta_info_table
     1.5  
     1.6        db.transaction {
     1.7 -        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
     1.8 +        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
     1.9          db.using_statement(table.insert())(stmt =>
    1.10          {
    1.11            db.set_string(stmt, 1, log_file.name)
    1.12 @@ -810,7 +810,7 @@
    1.13        val table = Data.sessions_table
    1.14  
    1.15        db.transaction {
    1.16 -        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.17 +        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
    1.18          db.using_statement(table.insert())(stmt =>
    1.19          {
    1.20            val entries_iterator =
    1.21 @@ -844,7 +844,7 @@
    1.22        val table = Data.ml_statistics_table
    1.23  
    1.24        db.transaction {
    1.25 -        db.using_statement(table.delete(Data.log_name.sql_where_equal(log_file.name)))(_.execute)
    1.26 +        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
    1.27          db.using_statement(table.insert())(stmt =>
    1.28          {
    1.29            val ml_stats: List[(String, Option[Bytes])] =
    1.30 @@ -896,7 +896,7 @@
    1.31      {
    1.32        val table = Data.meta_info_table
    1.33        val columns = table.columns.tail
    1.34 -      db.using_statement(table.select(columns, Data.log_name.sql_where_equal(log_name)))(stmt =>
    1.35 +      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
    1.36        {
    1.37          val rs = stmt.executeQuery
    1.38          if (!rs.next) None
    1.39 @@ -925,7 +925,7 @@
    1.40        val table2 = Data.ml_statistics_table
    1.41  
    1.42        val where_log_name =
    1.43 -        Data.log_name(table1).sql_where_equal(log_name) + " AND " +
    1.44 +        Data.log_name(table1).where_equal(log_name) + " AND " +
    1.45            Data.session_name(table1).ident + " <> ''"
    1.46        val where =
    1.47          if (session_names.isEmpty) where_log_name
     2.1 --- a/src/Pure/General/sql.scala	Wed May 03 15:51:34 2017 +0200
     2.2 +++ b/src/Pure/General/sql.scala	Wed May 03 15:53:23 2017 +0200
     2.3 @@ -106,8 +106,7 @@
     2.4      def sql_decl(sql_type: Type.Value => String): String =
     2.5        ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
     2.6  
     2.7 -    def sql_where_eq: String = "WHERE " + ident + " = "
     2.8 -    def sql_where_equal(s: String): String = sql_where_eq + string(s)
     2.9 +    def where_equal(s: String): String = "WHERE " + ident + " = " + string(s)
    2.10  
    2.11      override def toString: String = sql_decl(sql_type_default)
    2.12    }
     3.1 --- a/src/Pure/Thy/sessions.scala	Wed May 03 15:51:34 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Wed May 03 15:53:23 2017 +0200
     3.3 @@ -764,7 +764,7 @@
     3.4  
     3.5      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
     3.6        db.using_statement(Session_Info.table.select(List(column),
     3.7 -        Session_Info.session_name.sql_where_equal(name)))(stmt =>
     3.8 +        Session_Info.session_name.where_equal(name)))(stmt =>
     3.9        {
    3.10          val rs = stmt.executeQuery
    3.11          if (!rs.next) Bytes.empty else db.bytes(rs, column)
    3.12 @@ -822,7 +822,7 @@
    3.13        db.transaction {
    3.14          db.create_table(Session_Info.table)
    3.15          db.using_statement(
    3.16 -          Session_Info.table.delete(Session_Info.session_name.sql_where_equal(name)))(_.execute)
    3.17 +          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    3.18          db.using_statement(Session_Info.table.insert())(stmt =>
    3.19          {
    3.20            db.set_string(stmt, 1, name)
    3.21 @@ -865,7 +865,7 @@
    3.22  
    3.23      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    3.24        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    3.25 -        Session_Info.session_name.sql_where_equal(name)))(stmt =>
    3.26 +        Session_Info.session_name.where_equal(name)))(stmt =>
    3.27        {
    3.28          val rs = stmt.executeQuery
    3.29          if (!rs.next) None