# HG changeset patch
# User wenzelm
# Date 1489925106 -3600
# Node ID 52861eebf58d5f3998ce6272618437f81100d96b
# Parent  64da14387b2c7a10789836bf39102cf563061a7b
access table via session_name: db may in principle contain multiple entries;

diff -r 64da14387b2c -r 52861eebf58d src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Mar 19 12:57:29 2017 +0100
+++ b/src/Pure/Admin/build_history.scala	Sun Mar 19 13:05:06 2017 +0100
@@ -230,7 +230,7 @@
             val properties =
               if (database.is_file) {
                 using(SQLite.open_database(database))(db =>
-                  store.read_build_log(db, ml_statistics = true)).ml_statistics
+                  store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
               }
               else if (log_gz.is_file) {
                 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
diff -r 64da14387b2c -r 52861eebf58d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Mar 19 12:57:29 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 13:05:06 2017 +0100
@@ -9,6 +9,7 @@
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
+import java.sql.PreparedStatement
 
 import scala.collection.SortedSet
 import scala.collection.mutable
@@ -534,6 +535,16 @@
     val build_columns = List(sources, input_heaps, output_heap, return_code)
 
     val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
+
+    def where_session_name(name: String): String =
+      "WHERE " + SQL.quote_ident(session_name.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))
+
+    def delete_statement(db: SQL.Database, name: String): PreparedStatement =
+      db.delete_statement(table, where_session_name(name))
   }
 
   def store(system_mode: Boolean = false): Store = new Store(system_mode)
@@ -571,22 +582,15 @@
           map(xml_cache.props(_))
     }
 
-    def read_string(db: SQL.Database, table: SQL.Table, column: SQL.Column): String =
-      using(db.select_statement(table, List(column)))(stmt =>
-      {
-        val rs = stmt.executeQuery
-        if (!rs.next) "" else db.string(rs, column.name)
-      })
-
-    def read_bytes(db: SQL.Database, table: SQL.Table, column: SQL.Column): Bytes =
-      using(db.select_statement(table, List(column)))(stmt =>
+    def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
+      using(Session_Info.select_statement(db, name, List(column)))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) Bytes.empty else db.bytes(rs, column.name)
       })
 
-    def read_properties(db: SQL.Database, table: SQL.Table, column: SQL.Column)
-      : List[Properties.T] = uncompress_properties(read_bytes(db, table, column))
+    def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
+      uncompress_properties(read_bytes(db, name, column))
 
 
     /* output */
@@ -630,16 +634,16 @@
 
     def write_session_info(
       db: SQL.Database,
-      session_name: String,
+      name: String,
       build_log: Build_Log.Session_Info,
       build: Build.Session_Info)
     {
       db.transaction {
-        db.drop_table(Session_Info.table)
         db.create_table(Session_Info.table)
+        using(Session_Info.delete_statement(db, name))(_.execute)
         using(db.insert_statement(Session_Info.table))(stmt =>
         {
-          db.set_string(stmt, 1, session_name)
+          db.set_string(stmt, 1, name)
           db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
           db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
           db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
@@ -653,32 +657,32 @@
       }
     }
 
-    def read_session_timing(db: SQL.Database): Properties.T =
-      decode_properties(read_bytes(db, Session_Info.table, Session_Info.session_timing))
+    def read_session_timing(db: SQL.Database, name: String): Properties.T =
+      decode_properties(read_bytes(db, name, Session_Info.session_timing))
 
-    def read_command_timings(db: SQL.Database): List[Properties.T] =
-      read_properties(db, Session_Info.table, Session_Info.command_timings)
+    def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
+      read_properties(db, name, Session_Info.command_timings)
 
-    def read_ml_statistics(db: SQL.Database): List[Properties.T] =
-      read_properties(db, Session_Info.table, Session_Info.ml_statistics)
+    def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
+      read_properties(db, name, Session_Info.ml_statistics)
 
-    def read_task_statistics(db: SQL.Database): List[Properties.T] =
-      read_properties(db, Session_Info.table, Session_Info.task_statistics)
+    def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
+      read_properties(db, name, Session_Info.task_statistics)
 
-    def read_build_log(db: SQL.Database,
+    def read_build_log(db: SQL.Database, name: String,
       command_timings: Boolean = false,
       ml_statistics: Boolean = false,
       task_statistics: Boolean = false): Build_Log.Session_Info =
     {
       Build_Log.Session_Info(
-        session_timing = read_session_timing(db),
-        command_timings = if (command_timings) read_command_timings(db) else Nil,
-        ml_statistics = if (ml_statistics) read_ml_statistics(db) else Nil,
-        task_statistics = if (task_statistics) read_task_statistics(db) else Nil)
+        session_timing = read_session_timing(db, name),
+        command_timings = if (command_timings) read_command_timings(db, name) else Nil,
+        ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
+        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil)
     }
 
-    def read_build(db: SQL.Database): Option[Build.Session_Info] =
-      using(db.select_statement(Session_Info.table, Session_Info.build_columns))(stmt =>
+    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
+      using(Session_Info.select_statement(db, name, Session_Info.build_columns))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None
diff -r 64da14387b2c -r 52861eebf58d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Mar 19 12:57:29 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sun Mar 19 13:05:06 2017 +0100
@@ -49,7 +49,7 @@
           try {
             using(SQLite.open_database(database))(db =>
             {
-              val build_log = store.read_build_log(db, command_timings = true)
+              val build_log = store.read_build_log(db, name, command_timings = true)
               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
               (build_log.command_timings, session_timing)
             })
@@ -525,7 +525,7 @@
                 {
                   store.find_database_heap(name) match {
                     case Some((database, heap_stamp)) =>
-                      using(SQLite.open_database(database))(store.read_build(_)) match {
+                      using(SQLite.open_database(database))(store.read_build(_, name)) match {
                         case Some(build) =>
                           val current =
                             build.sources == sources_stamp(name) &&