--- 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] =
--- 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
}
}
}