# HG changeset patch
# User wenzelm
# Date 1493378463 -7200
# Node ID 637aa8e93cd7f9ab7add10ba07ee09d7031357ca
# Parent  d6fe8a277576e129fd2473e069d76e503043339e
tuned;

diff -r d6fe8a277576 -r 637aa8e93cd7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 28 13:18:06 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 13:21:03 2017 +0200
@@ -747,13 +747,6 @@
     val build_columns = List(sources, input_heaps, output_heap, return_code)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
-
-    def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
-        : PreparedStatement =
-      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_equal(name))
   }
 
   def store(system_mode: Boolean = false): Store = new Store(system_mode)
@@ -770,7 +763,8 @@
     /* SQL database content */
 
     def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
-      using(Session_Info.select_statement(db, name, List(column)))(stmt =>
+      using(db.select_statement(Session_Info.table, List(column),
+        Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) Bytes.empty else db.bytes(rs, column)
@@ -827,7 +821,8 @@
     {
       db.transaction {
         db.create_table(Session_Info.table)
-        using(Session_Info.delete_statement(db, name))(_.execute)
+        using(db.delete_statement(Session_Info.table,
+          Session_Info.session_name.sql_where_equal(name)))(_.execute)
         using(db.insert_statement(Session_Info.table))(stmt =>
         {
           db.set_string(stmt, 1, name)
@@ -869,7 +864,8 @@
     }
 
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
-      using(Session_Info.select_statement(db, name, Session_Info.build_columns))(stmt =>
+      using(db.select_statement(Session_Info.table, Session_Info.build_columns,
+        Session_Info.session_name.sql_where_equal(name)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None