access table via session_name: db may in principle contain multiple entries;
authorwenzelm
Sun Mar 19 13:05:06 2017 +0100 (2017-03-19)
changeset 6532052861eebf58d
parent 65319 64da14387b2c
child 65321 2b1cd063e0b2
access table via session_name: db may in principle contain multiple entries;
src/Pure/Admin/build_history.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Sun Mar 19 12:57:29 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_history.scala	Sun Mar 19 13:05:06 2017 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4              val properties =
     1.5                if (database.is_file) {
     1.6                  using(SQLite.open_database(database))(db =>
     1.7 -                  store.read_build_log(db, ml_statistics = true)).ml_statistics
     1.8 +                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
     1.9                }
    1.10                else if (log_gz.is_file) {
    1.11                  Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
     2.1 --- a/src/Pure/Thy/sessions.scala	Sun Mar 19 12:57:29 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 13:05:06 2017 +0100
     2.3 @@ -9,6 +9,7 @@
     2.4  import java.nio.ByteBuffer
     2.5  import java.nio.channels.FileChannel
     2.6  import java.nio.file.StandardOpenOption
     2.7 +import java.sql.PreparedStatement
     2.8  
     2.9  import scala.collection.SortedSet
    2.10  import scala.collection.mutable
    2.11 @@ -534,6 +535,16 @@
    2.12      val build_columns = List(sources, input_heaps, output_heap, return_code)
    2.13  
    2.14      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    2.15 +
    2.16 +    def where_session_name(name: String): String =
    2.17 +      "WHERE " + SQL.quote_ident(session_name.name) + " = " + SQL.quote_string(name)
    2.18 +
    2.19 +    def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column])
    2.20 +        : PreparedStatement =
    2.21 +      db.select_statement(table, columns, where_session_name(name))
    2.22 +
    2.23 +    def delete_statement(db: SQL.Database, name: String): PreparedStatement =
    2.24 +      db.delete_statement(table, where_session_name(name))
    2.25    }
    2.26  
    2.27    def store(system_mode: Boolean = false): Store = new Store(system_mode)
    2.28 @@ -571,22 +582,15 @@
    2.29            map(xml_cache.props(_))
    2.30      }
    2.31  
    2.32 -    def read_string(db: SQL.Database, table: SQL.Table, column: SQL.Column): String =
    2.33 -      using(db.select_statement(table, List(column)))(stmt =>
    2.34 -      {
    2.35 -        val rs = stmt.executeQuery
    2.36 -        if (!rs.next) "" else db.string(rs, column.name)
    2.37 -      })
    2.38 -
    2.39 -    def read_bytes(db: SQL.Database, table: SQL.Table, column: SQL.Column): Bytes =
    2.40 -      using(db.select_statement(table, List(column)))(stmt =>
    2.41 +    def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
    2.42 +      using(Session_Info.select_statement(db, name, List(column)))(stmt =>
    2.43        {
    2.44          val rs = stmt.executeQuery
    2.45          if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
    2.46        })
    2.47  
    2.48 -    def read_properties(db: SQL.Database, table: SQL.Table, column: SQL.Column)
    2.49 -      : List[Properties.T] = uncompress_properties(read_bytes(db, table, column))
    2.50 +    def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
    2.51 +      uncompress_properties(read_bytes(db, name, column))
    2.52  
    2.53  
    2.54      /* output */
    2.55 @@ -630,16 +634,16 @@
    2.56  
    2.57      def write_session_info(
    2.58        db: SQL.Database,
    2.59 -      session_name: String,
    2.60 +      name: String,
    2.61        build_log: Build_Log.Session_Info,
    2.62        build: Build.Session_Info)
    2.63      {
    2.64        db.transaction {
    2.65 -        db.drop_table(Session_Info.table)
    2.66          db.create_table(Session_Info.table)
    2.67 +        using(Session_Info.delete_statement(db, name))(_.execute)
    2.68          using(db.insert_statement(Session_Info.table))(stmt =>
    2.69          {
    2.70 -          db.set_string(stmt, 1, session_name)
    2.71 +          db.set_string(stmt, 1, name)
    2.72            db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
    2.73            db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
    2.74            db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
    2.75 @@ -653,32 +657,32 @@
    2.76        }
    2.77      }
    2.78  
    2.79 -    def read_session_timing(db: SQL.Database): Properties.T =
    2.80 -      decode_properties(read_bytes(db, Session_Info.table, Session_Info.session_timing))
    2.81 +    def read_session_timing(db: SQL.Database, name: String): Properties.T =
    2.82 +      decode_properties(read_bytes(db, name, Session_Info.session_timing))
    2.83  
    2.84 -    def read_command_timings(db: SQL.Database): List[Properties.T] =
    2.85 -      read_properties(db, Session_Info.table, Session_Info.command_timings)
    2.86 +    def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
    2.87 +      read_properties(db, name, Session_Info.command_timings)
    2.88  
    2.89 -    def read_ml_statistics(db: SQL.Database): List[Properties.T] =
    2.90 -      read_properties(db, Session_Info.table, Session_Info.ml_statistics)
    2.91 +    def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
    2.92 +      read_properties(db, name, Session_Info.ml_statistics)
    2.93  
    2.94 -    def read_task_statistics(db: SQL.Database): List[Properties.T] =
    2.95 -      read_properties(db, Session_Info.table, Session_Info.task_statistics)
    2.96 +    def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
    2.97 +      read_properties(db, name, Session_Info.task_statistics)
    2.98  
    2.99 -    def read_build_log(db: SQL.Database,
   2.100 +    def read_build_log(db: SQL.Database, name: String,
   2.101        command_timings: Boolean = false,
   2.102        ml_statistics: Boolean = false,
   2.103        task_statistics: Boolean = false): Build_Log.Session_Info =
   2.104      {
   2.105        Build_Log.Session_Info(
   2.106 -        session_timing = read_session_timing(db),
   2.107 -        command_timings = if (command_timings) read_command_timings(db) else Nil,
   2.108 -        ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
   2.109 -        task_statistics = if (task_statistics) read_task_statistics(db) else Nil)
   2.110 +        session_timing = read_session_timing(db, name),
   2.111 +        command_timings = if (command_timings) read_command_timings(db, name) else Nil,
   2.112 +        ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
   2.113 +        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil)
   2.114      }
   2.115  
   2.116 -    def read_build(db: SQL.Database): Option[Build.Session_Info] =
   2.117 -      using(db.select_statement(Session_Info.table, Session_Info.build_columns))(stmt =>
   2.118 +    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
   2.119 +      using(Session_Info.select_statement(db, name, Session_Info.build_columns))(stmt =>
   2.120        {
   2.121          val rs = stmt.executeQuery
   2.122          if (!rs.next) None
     3.1 --- a/src/Pure/Tools/build.scala	Sun Mar 19 12:57:29 2017 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Sun Mar 19 13:05:06 2017 +0100
     3.3 @@ -49,7 +49,7 @@
     3.4            try {
     3.5              using(SQLite.open_database(database))(db =>
     3.6              {
     3.7 -              val build_log = store.read_build_log(db, command_timings = true)
     3.8 +              val build_log = store.read_build_log(db, name, command_timings = true)
     3.9                val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    3.10                (build_log.command_timings, session_timing)
    3.11              })
    3.12 @@ -525,7 +525,7 @@
    3.13                  {
    3.14                    store.find_database_heap(name) match {
    3.15                      case Some((database, heap_stamp)) =>
    3.16 -                      using(SQLite.open_database(database))(store.read_build(_)) match {
    3.17 +                      using(SQLite.open_database(database))(store.read_build(_, name)) match {
    3.18                          case Some(build) =>
    3.19                            val current =
    3.20                              build.sources == sources_stamp(name) &&