# HG changeset patch
# User wenzelm
# Date 1489744712 -3600
# Node ID b661543a0de69c394b6a32d5a33835542c17c115
# Parent  92bc225c76331636e0df5a69f5c1db629c285ecc
clarified signature;

diff -r 92bc225c7633 -r b661543a0de6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 17 10:39:14 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 10:58:32 2017 +0100
@@ -526,7 +526,7 @@
     def log_gz(name: String): Path = log(name).ext("gz")
 
 
-    /* SQL data representation */
+    /* SQL database content */
 
     val xml_cache: XML.Cache = new XML.Cache()
 
@@ -550,17 +550,19 @@
           map(xml_cache.props(_))
     }
 
-    def read_properties(db: SQLite.Database, table: SQL.Table, column: SQL.Column)
-      : List[Properties.T] =
+    def read_bytes(db: SQLite.Database, table: SQL.Table, column: SQL.Column): Bytes =
     {
       using(db.select_statement(table, List(column)))(stmt =>
       {
         val rs = stmt.executeQuery
-        if (!rs.next) Nil
-        else uncompress_properties(db.bytes(rs, column.name))
+        if (!rs.next) Bytes.empty
+        else db.bytes(rs, column.name)
       })
     }
 
+    def read_properties(db: SQLite.Database, table: SQL.Table, column: SQL.Column)
+      : List[Properties.T] = uncompress_properties(read_bytes(db, table, column))
+
 
     /* output */
 
@@ -651,6 +653,18 @@
       }
     }
 
+    def read_session_timing(store: Store, db: SQLite.Database): Properties.T =
+      store.decode_properties(store.read_bytes(db, table, session_timing))
+
+    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)
+
     def read_build_log(store: Store, db: SQLite.Database): Option[Build_Log.Session_Info] =
       using(db.select_statement(table, build_log_columns))(stmt =>
       {
@@ -681,12 +695,5 @@
               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)
   }
 }