# HG changeset patch
# User wenzelm
# Date 1708265027 -3600
# Node ID dca6ea3b7a015a4ad3d80226c4c0bf7d4c0c6a97
# Parent  2a9d8c74eb3c4ffc1cfd1545bef1131588e839a0
clarified signature: more explicit types;

diff -r 2a9d8c74eb3c -r dca6ea3b7a01 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sun Feb 18 13:32:44 2024 +0100
+++ b/src/Pure/Build/store.scala	Sun Feb 18 15:03:47 2024 +0100
@@ -15,6 +15,16 @@
     new Store(options, cache)
 
 
+  /* session */
+
+  sealed case class Session(name: String, heap: Option[Path], log_db: Option[Path]) {
+    def defined: Boolean = heap.isDefined || log_db.isDefined
+
+    override def toString: String = name
+  }
+
+
+
   /* session build info */
 
   sealed case class Build_Info(
@@ -263,6 +273,12 @@
   def output_log_gz(name: String): Path = output_dir + log_gz(name)
 
 
+  /* session */
+
+  def get_session(name: String): Store.Session =
+    Store.Session(name, find_heap(name), find_log_db(name))
+
+
   /* heap */
 
   def find_heap(name: String): Option[Path] =
diff -r 2a9d8c74eb3c -r dca6ea3b7a01 src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sun Feb 18 13:32:44 2024 +0100
+++ b/src/Pure/Tools/sync.scala	Sun Feb 18 15:03:47 2024 +0100
@@ -17,15 +17,16 @@
     else {
       val store = Store(options)
       val sessions_structure = Sessions.load_structure(options, dirs = dirs)
-      sessions_structure.build_requirements(session_images).flatMap { session =>
+      sessions_structure.build_requirements(session_images).flatMap { name =>
+        val session = store.get_session(name)
         val heap =
-          store.find_heap(session).map(_.expand).map(path =>
+          session.heap.map(_.expand).map(path =>
             File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
-        val db =
-          store.find_log_db(session).map(_.expand).map(path =>
+        val log_db =
+          session.log_db.map(_.expand).map(path =>
             File.standard_path(path.dir.dir.dir) + "/./" + path.dir.dir.file_name + "/" +
               path.dir.file_name + "/" + path.file_name)
-        heap.toList ::: db.toList
+        heap.toList ::: log_db.toList
       }
     }
   }