# HG changeset patch
# User wenzelm
# Date 1677675131 -3600
# Node ID d6bf9ec39d1292b9a83aa5f319f7efef85432c03
# Parent  0030eabbe6c3d68c3fb5f9c69d9e5a59773ef52c
avoid premature Properties.uncompress: allow blob to be stored in another database;

diff -r 0030eabbe6c3 -r d6bf9ec39d12 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 01 13:30:35 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 01 13:52:11 2023 +0100
@@ -1591,8 +1591,8 @@
     def read_session_timing(db: SQL.Database, name: String): Properties.T =
       Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
 
-    def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
-      read_properties(db, name, Session_Info.command_timings)
+    def read_command_timings(db: SQL.Database, name: String): Bytes =
+      read_bytes(db, name, Session_Info.command_timings)
 
     def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.theory_timings)
diff -r 0030eabbe6c3 -r d6bf9ec39d12 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 13:30:35 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 13:52:11 2023 +0100
@@ -17,7 +17,7 @@
 
   object Session_Context {
     def empty(session: String, timeout: Time): Session_Context =
-      new Session_Context(session, timeout, Time.zero, Nil)
+      new Session_Context(session, timeout, Time.zero, Bytes.empty)
 
     def apply(
       session: String,
@@ -56,9 +56,10 @@
     val session: String,
     val timeout: Time,
     val old_time: Time,
-    val old_command_timings: List[Properties.T]
+    val old_command_timings_blob: Bytes
   ) {
-    def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty
+    def is_empty: Boolean =
+      old_time.is_zero && old_command_timings_blob.is_empty
 
     override def toString: String = session
   }
@@ -149,6 +150,9 @@
     def apply(session: String): Session_Context =
       sessions.getOrElse(session, Session_Context.empty(session, Time.zero))
 
+    def old_command_timings(session: String): List[Properties.T] =
+      Properties.uncompress(apply(session).old_command_timings_blob, cache = store.cache)
+
     def do_store(session: String): Boolean =
       build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)
   }
@@ -652,7 +656,7 @@
 
       val resources =
         new Resources(session_background, log = log,
-          command_timings = build_context(session_name).old_command_timings)
+          command_timings = build_context.old_command_timings(session_name))
 
       val job =
         synchronized {