src/Pure/Thy/sessions.scala
changeset 65604 637aa8e93cd7
parent 65602 d9533e9615ad
child 65619 e33b3d57b7cb
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 28 13:18:06 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 28 13:21:03 2017 +0200
     1.3 @@ -747,13 +747,6 @@
     1.4      val build_columns = List(sources, input_heaps, output_heap, return_code)
     1.5  
     1.6      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
     1.7 -
     1.8 -    def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
     1.9 -        : PreparedStatement =
    1.10 -      db.select_statement(table, columns, session_name.sql_where_equal(name))
    1.11 -
    1.12 -    def delete_statement(db: SQL.Database, name: String): PreparedStatement =
    1.13 -      db.delete_statement(table, session_name.sql_where_equal(name))
    1.14    }
    1.15  
    1.16    def store(system_mode: Boolean = false): Store = new Store(system_mode)
    1.17 @@ -770,7 +763,8 @@
    1.18      /* SQL database content */
    1.19  
    1.20      def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    1.21 -      using(Session_Info.select_statement(db, name, List(column)))(stmt =>
    1.22 +      using(db.select_statement(Session_Info.table, List(column),
    1.23 +        Session_Info.session_name.sql_where_equal(name)))(stmt =>
    1.24        {
    1.25          val rs = stmt.executeQuery
    1.26          if (!rs.next) Bytes.empty else db.bytes(rs, column)
    1.27 @@ -827,7 +821,8 @@
    1.28      {
    1.29        db.transaction {
    1.30          db.create_table(Session_Info.table)
    1.31 -        using(Session_Info.delete_statement(db, name))(_.execute)
    1.32 +        using(db.delete_statement(Session_Info.table,
    1.33 +          Session_Info.session_name.sql_where_equal(name)))(_.execute)
    1.34          using(db.insert_statement(Session_Info.table))(stmt =>
    1.35          {
    1.36            db.set_string(stmt, 1, name)
    1.37 @@ -869,7 +864,8 @@
    1.38      }
    1.39  
    1.40      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.41 -      using(Session_Info.select_statement(db, name, Session_Info.build_columns))(stmt =>
    1.42 +      using(db.select_statement(Session_Info.table, Session_Info.build_columns,
    1.43 +        Session_Info.session_name.sql_where_equal(name)))(stmt =>
    1.44        {
    1.45          val rs = stmt.executeQuery
    1.46          if (!rs.next) None