# HG changeset patch
# User wenzelm
# Date 1708279745 -3600
# Node ID 215db9299a1a6c320835cc6b7f736c95dfd4eb46
# Parent  26fa2e8761fb517cc9e213563b18075de571bebc
clarified signature;

diff -r 26fa2e8761fb -r 215db9299a1a src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Sun Feb 18 15:16:20 2024 +0100
+++ b/src/Pure/Build/store.scala	Sun Feb 18 19:09:05 2024 +0100
@@ -17,9 +17,19 @@
 
   /* session */
 
-  sealed case class Session(name: String, heap: Option[Path], log_db: Option[Path]) {
+  final class Session private[Store](
+    val name: String,
+    val heap: Option[Path],
+    val log_db: Option[Path],
+    dirs: List[Path]
+  ) {
     def defined: Boolean = heap.isDefined || log_db.isDefined
 
+    def the_heap: Path =
+      heap getOrElse
+        error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
+          cat_lines(dirs.map(dir => "  " + File.standard_path(dir))))
+
     def heap_digest(): Option[SHA1.Digest] =
       heap.flatMap(ML_Heap.read_file_digest)
 
@@ -281,17 +291,12 @@
   def get_session(name: String): Store.Session = {
     val heap = input_dirs.view.map(_ + store.heap(name)).find(_.is_file)
     val log_db = input_dirs.view.map(_ + store.log_db(name)).find(_.is_file)
-    Store.Session(name, heap, log_db)
+    new Store.Session(name, heap, log_db, input_dirs)
   }
 
 
   /* heap */
 
-  def the_heap(name: String): Path =
-    get_session(name).heap getOrElse
-      error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
-        cat_lines(input_dirs.map(dir => "  " + File.standard_path(dir))))
-
   def heap_shasum(database_server: Option[SQL.Database], name: String): SHA1.Shasum = {
     def get_database: Option[SHA1.Digest] = {
       for {
diff -r 26fa2e8761fb -r 215db9299a1a src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun Feb 18 15:16:20 2024 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Feb 18 19:09:05 2024 +0100
@@ -24,7 +24,7 @@
 
     session_background.sessions_structure.selection(logic_name).
       build_requirements(List(logic_name)).
-      map(store.the_heap)
+      map(name => store.get_session(name).the_heap)
   }
 
   def apply(
diff -r 26fa2e8761fb -r 215db9299a1a src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Sun Feb 18 15:16:20 2024 +0100
+++ b/src/Pure/Tools/profiling.scala	Sun Feb 18 19:09:05 2024 +0100
@@ -99,7 +99,7 @@
         locales = session.locales,
         locale_thms = session.locale_thms,
         global_thms = session.global_thms,
-        heap_size = File.space(store.the_heap(session_name)),
+        heap_size = File.space(store.get_session(session_name).the_heap),
         thys_id_size = session.sizeof_thys_id,
         thms_id_size = session.sizeof_thms_id,
         terms_size = session.sizeof_terms,