# HG changeset patch
# User wenzelm
# Date 1687271953 -7200
# Node ID 02c5488b8c9cd2f9e4bfce98394d4f48b4728585
# Parent  a49ad8d183af9d47e8bd01aa01eb813b0fad601c
tuned signature;

diff -r a49ad8d183af -r 02c5488b8c9c src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Tue Jun 20 15:00:45 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 20 16:39:13 2023 +0200
@@ -137,7 +137,7 @@
 
     def read_sources(
       db: SQL.Database,
-      cache: Term.Cache,
+      cache: Compress.Cache,
       session_name: String,
       name: String = ""
     ): List[Source_File] = {
@@ -150,7 +150,7 @@
           val digest = SHA1.fake_digest(res.string(Sources.digest))
           val compressed = res.bool(Sources.compressed)
           val body = res.bytes(Sources.body)
-          Source_File(res_name, digest, compressed, body, cache.compress)
+          Source_File(res_name, digest, compressed, body, cache)
         }
       )
     }
@@ -437,5 +437,5 @@
   }
 
   def read_sources(db: SQL.Database, session: String, name: String = ""): List[Store.Source_File] =
-    Store.Data.read_sources(db, cache, session, name = name)
+    Store.Data.read_sources(db, cache.compress, session, name = name)
 }