# HG changeset patch
# User wenzelm
# Date 1489743554 -3600
# Node ID 92bc225c76331636e0df5a69f5c1db629c285ecc
# Parent  d189ff34b5b9614cf2088a26854f4a5655df39cd
more selective queries;

diff -r d189ff34b5b9 -r 92bc225c7633 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 17 10:03:00 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 10:39:14 2017 +0100
@@ -526,7 +526,7 @@
     def log_gz(name: String): Path = log(name).ext("gz")
 
 
-    /* data representation */
+    /* SQL data representation */
 
     val xml_cache: XML.Cache = new XML.Cache()
 
@@ -550,6 +550,17 @@
           map(xml_cache.props(_))
     }
 
+    def read_properties(db: SQLite.Database, table: SQL.Table, column: SQL.Column)
+      : List[Properties.T] =
+    {
+      using(db.select_statement(table, List(column)))(stmt =>
+      {
+        val rs = stmt.executeQuery
+        if (!rs.next) Nil
+        else uncompress_properties(db.bytes(rs, column.name))
+      })
+    }
+
 
     /* output */
 
@@ -606,18 +617,19 @@
     val command_timings = SQL.Column.bytes("command_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
+    val build_log_columns =
+      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
     val return_code = SQL.Column.int("return_code")
+    val build_columns = List(sources, input_heaps, output_heap, return_code)
 
-    val table = SQL.Table("isabelle_session_info",
-      List(session_name, session_timing, command_timings, ml_statistics, task_statistics,
-        sources, input_heaps, output_heap, return_code))
+    val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
 
-    def write_data(store: Store, db: SQLite.Database,
+    def write(store: Store, db: SQLite.Database,
       build_log: Build_Log.Session_Info, build: Build.Session_Info)
     {
       db.transaction {
@@ -639,30 +651,42 @@
       }
     }
 
-    def read_data(store: Store, db: SQLite.Database)
-      : Option[(Build_Log.Session_Info, Build.Session_Info)] =
-    {
-      using(db.select_statement(table, table.columns))(stmt =>
+    def read_build_log(store: Store, db: SQLite.Database): Option[Build_Log.Session_Info] =
+      using(db.select_statement(table, build_log_columns))(stmt =>
       {
         val rs = stmt.executeQuery
         if (!rs.next) None
         else {
-          val build_log =
+          Some(
             Build_Log.Session_Info(
               db.string(rs, session_name.name),
               store.decode_properties(db.bytes(rs, session_timing.name)),
               store.uncompress_properties(db.bytes(rs, command_timings.name)),
               store.uncompress_properties(db.bytes(rs, ml_statistics.name)),
-              store.uncompress_properties(db.bytes(rs, task_statistics.name)))
-          val build =
+              store.uncompress_properties(db.bytes(rs, task_statistics.name))))
+        }
+      })
+
+    def read_build(store: Store, db: SQLite.Database): Option[Build.Session_Info] =
+      using(db.select_statement(table, table.columns))(stmt =>
+      {
+        val rs = stmt.executeQuery
+        if (!rs.next) None
+        else {
+          Some(
             Build.Session_Info(
               split_lines(db.string(rs, sources.name)),
               split_lines(db.string(rs, input_heaps.name)),
               db.string(rs, output_heap.name),
-              db.int(rs, return_code.name))
-          Some((build_log, build))
+              db.int(rs, return_code.name)))
         }
       })
-    }
+
+    def read_command_timings(store: Store, db: SQLite.Database): List[Properties.T] =
+      store.read_properties(db, table, command_timings)
+    def read_ml_statistics(store: Store, db: SQLite.Database): List[Properties.T] =
+      store.read_properties(db, table, ml_statistics)
+    def read_task_statistics(store: Store, db: SQLite.Database): List[Properties.T] =
+      store.read_properties(db, table, task_statistics)
   }
 }