tuned signature;
authorwenzelm
Thu Apr 27 11:41:13 2017 +0200 (2017-04-27)
changeset 65593607f7ad07a60
parent 65592 f45609debe0d
child 65594 659305708959
tuned signature;
src/Pure/General/sql.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/General/sql.scala	Thu Apr 27 11:26:25 2017 +0200
     1.2 +++ b/src/Pure/General/sql.scala	Thu Apr 27 11:41:13 2017 +0200
     1.3 @@ -91,6 +91,9 @@
     1.4      def sql_decl(sql_type: Type.Value => String): String =
     1.5        sql_name + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
     1.6  
     1.7 +    def sql_where_eq: String = "WHERE " + sql_name + " = "
     1.8 +    def sql_where_eq_string(s: String): String = sql_where_eq + quote_string(s)
     1.9 +
    1.10      override def toString: String = sql_decl(sql_type_default)
    1.11    }
    1.12  
     2.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 27 11:26:25 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 27 11:41:13 2017 +0200
     2.3 @@ -748,15 +748,12 @@
     2.4  
     2.5      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
     2.6  
     2.7 -    def where_session_name(name: String): String =
     2.8 -      "WHERE " + session_name.sql_name + " = " + SQL.quote_string(name)
     2.9 -
    2.10      def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
    2.11          : PreparedStatement =
    2.12 -      db.select_statement(table, columns, where_session_name(name))
    2.13 +      db.select_statement(table, columns, session_name.sql_where_eq_string(name))
    2.14  
    2.15      def delete_statement(db: SQL.Database, name: String): PreparedStatement =
    2.16 -      db.delete_statement(table, where_session_name(name))
    2.17 +      db.delete_statement(table, session_name.sql_where_eq_string(name))
    2.18    }
    2.19  
    2.20    def store(system_mode: Boolean = false): Store = new Store(system_mode)