# HG changeset patch
# User wenzelm
# Date 1672669093 -3600
# Node ID 165ba28378f6264eb27f700cab9cc1ee0a4013b9
# Parent  19bfc64a7310496b35a0e704e894a842de0509c9
clarified signature: more explicit types;

diff -r 19bfc64a7310 -r 165ba28378f6 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jan 02 15:05:15 2023 +0100
+++ b/src/Pure/Thy/export.scala	Mon Jan 02 15:18:13 2023 +0100
@@ -433,7 +433,7 @@
       def db_source: Option[String] =
         db_hierarchy.view.map(database =>
             database_context.store.read_sources(database.db, database.session, name.node))
-          .collectFirst({ case Some(bytes) => bytes.text })
+          .collectFirst({ case Some(file) => file.text })
       snapshot_source orElse db_source getOrElse ""
     }
 
diff -r 19bfc64a7310 -r 165ba28378f6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jan 02 15:05:15 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Jan 02 15:18:13 2023 +0100
@@ -57,7 +57,16 @@
 
   /* source files */
 
-  sealed case class Source_File(name: String, digest: SHA1.Digest, compressed: Boolean, body: Bytes)
+  sealed case class Source_File(
+    name: String,
+    digest: SHA1.Digest,
+    compressed: Boolean,
+    body: Bytes,
+    cache: Compress.Cache
+  ) {
+    def bytes: Bytes = if (compressed) body.uncompress(cache = cache) else body
+    def text: String = bytes.text
+  }
 
   object Sources {
     val session_name = SQL.Column.string("session_name").make_primary_key
@@ -88,7 +97,7 @@
               val bytes = Bytes.read(path)
               if (bytes.sha1_digest == digest) {
                 val (compressed, body) = bytes.maybe_compress(Compress.Options_Zstd(), cache = cache)
-                val file = Source_File(name, digest, compressed, body)
+                val file = Source_File(name, digest, compressed, body, cache)
                 sources + (name -> file)
               }
               else err(path)
@@ -1652,17 +1661,17 @@
       }
     }
 
-    def read_sources(db: SQL.Database, session_name: String, name: String): Option[Bytes] = {
+    def read_sources(db: SQL.Database, session_name: String, name: String): Option[Source_File] = {
       val sql =
-        Sources.table.select(List(Sources.compressed, Sources.body),
-          Sources.where_equal(session_name, name = name))
+        Sources.table.select(Nil, Sources.where_equal(session_name, name = name))
       db.using_statement(sql) { stmt =>
         val res = stmt.execute_query()
         if (!res.next()) None
         else {
+          val digest = SHA1.fake_digest(res.string(Sources.digest))
           val compressed = res.bool(Sources.compressed)
-          val bs = res.bytes(Sources.body)
-          Some(if (compressed) bs.uncompress(cache = cache.compress) else bs)
+          val body = res.bytes(Sources.body)
+          Some(Source_File(name, digest, compressed, body, cache.compress))
         }
       }
     }