# HG changeset patch
# User wenzelm
# Date 1493286073 -7200
# Node ID 607f7ad07a60c89eb3fbc6bed0ec111e16462c0a
# Parent  f45609debe0d8cd92c25ffa7d91c7dd3d42a08f7
tuned signature;

diff -r f45609debe0d -r 607f7ad07a60 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Apr 27 11:26:25 2017 +0200
+++ b/src/Pure/General/sql.scala	Thu Apr 27 11:41:13 2017 +0200
@@ -91,6 +91,9 @@
     def sql_decl(sql_type: Type.Value => String): String =
       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)
+
     override def toString: String = sql_decl(sql_type_default)
   }
 
diff -r f45609debe0d -r 607f7ad07a60 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 27 11:26:25 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 27 11:41:13 2017 +0200
@@ -748,15 +748,12 @@
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
 
-    def where_session_name(name: String): String =
-      "WHERE " + session_name.sql_name + " = " + SQL.quote_string(name)
-
     def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
         : PreparedStatement =
-      db.select_statement(table, columns, where_session_name(name))
+      db.select_statement(table, columns, session_name.sql_where_eq_string(name))
 
     def delete_statement(db: SQL.Database, name: String): PreparedStatement =
-      db.delete_statement(table, where_session_name(name))
+      db.delete_statement(table, session_name.sql_where_eq_string(name))
   }
 
   def store(system_mode: Boolean = false): Store = new Store(system_mode)