# HG changeset patch
# User wenzelm
# Date 1750795700 -7200
# Node ID 20ffc02d0b0e4bc503985984f9bb20847d67d4d3
# Parent  84534cc9c97e47d8e99e461a20c4bc1d2fc40f9f
clarified modules;

diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Build/build_benchmark.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -68,7 +68,7 @@
         def get_shasum(name: String): SHA1.Shasum =
           store.check_output(database_server, name,
             sources_shasum = sessions(name).sources_shasum,
-            input_shasum = ML_Process.make_shasum(store, sessions(name).ancestors.map(get_shasum)),
+            input_shasum = store.make_shasum(sessions(name).ancestors.map(get_shasum)),
             build_thorough = build_context.sessions_structure(name).build_thorough)._2
 
         val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -134,7 +134,7 @@
           val session_heaps =
             session_background.info.parent match {
               case None => Nil
-              case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
+              case Some(logic) => store.session_heaps(session_background, logic = logic)
             }
 
           val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Build/build_process.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -1161,7 +1161,7 @@
     ancestor_results: List[Build_Process.Result]
   ): Build_Process.State = {
     val sources_shasum = state.sessions(session_name).sources_shasum
-    val input_shasum = ML_Process.make_shasum(store, ancestor_results.map(_.output_shasum))
+    val input_shasum = store.make_shasum(ancestor_results.map(_.output_shasum))
     val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
     val (current, output_shasum) =
       store.check_output(_database_server, session_name,
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Build/build_schedule.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -1132,7 +1132,7 @@
           store.check_output(
             _database_server, session_name,
             sources_shasum = state.sessions(session_name).sources_shasum,
-            input_shasum = ML_Process.make_shasum(store, ancestor_results.map(_.output_shasum)),
+            input_shasum = store.make_shasum(ancestor_results.map(_.output_shasum)),
             build_thorough = build_context.sessions_structure(session_name).build_thorough,
             fresh_build = build_context.fresh_build,
             store_heap = build_context.store_heap || state.sessions.store_heap(session_name))._1
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Build/store.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -323,7 +323,7 @@
   def output_log_gz(name: String): Path = output_dir + Store.log_gz(name)
 
 
-  /* session */
+  /* session heaps */
 
   def get_session(name: String): Store.Session = {
     val heap = input_dirs.view.map(_ + Store.heap(name)).find(_.is_file)
@@ -337,8 +337,23 @@
     new Store.Session(name, heap, log_db, List(output_dir))
   }
 
+  def session_heaps(
+    session_background: Sessions.Background,
+    logic: String = ""
+  ): List[Path] = {
+    val logic_name = Isabelle_System.default_logic(logic)
 
-  /* heap */
+    session_background.sessions_structure.selection(logic_name).
+      build_requirements(List(logic_name)).
+      map(name => store.get_session(name).the_heap)
+  }
+
+
+  /* heap shasum */
+
+  def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
+    if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(ml_settings.polyml_exe))
+    else SHA1.flat_shasum(ancestors)
 
   def heap_shasum(database_server: Option[SQL.Database], name: String): SHA1.Shasum = {
     def get_database: Option[SHA1.Digest] = {
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/ML/ml_console.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -73,7 +73,7 @@
 
       val session_heaps =
         if (raw_ml_system) Nil
-        else ML_Process.session_heaps(store, session_background, logic = logic)
+        else store.session_heaps(session_background, logic = logic)
 
       // process loop
       val process =
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -11,25 +11,6 @@
 
 
 object ML_Process {
-  /* heaps */
-
-  def make_shasum(store: Store, ancestors: List[SHA1.Shasum]): SHA1.Shasum =
-    if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(store.ml_settings.polyml_exe))
-    else SHA1.flat_shasum(ancestors)
-
-  def session_heaps(
-    store: Store,
-    session_background: Sessions.Background,
-    logic: String = ""
-  ): List[Path] = {
-    val logic_name = Isabelle_System.default_logic(logic)
-
-    session_background.sessions_structure.selection(logic_name).
-      build_requirements(List(logic_name)).
-      map(name => store.get_session(name).the_heap)
-  }
-
-
   /* process */
 
   def apply(
@@ -186,7 +167,7 @@
 
       val store = Store(options)
       val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
-      val session_heaps = ML_Process.session_heaps(store, session_background, logic = logic)
+      val session_heaps = store.session_heaps(session_background, logic = logic)
       val result =
         ML_Process(options, session_background, session_heaps, args = eval_args, modes = modes)
           .result(
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -621,7 +621,7 @@
       val session_name = session_background.session_name
       val session = new Session(session_name, options, resources)
 
-      val session_heaps = ML_Process.session_heaps(store, session_background, logic = session_name)
+      val session_heaps = store.session_heaps(session_background, logic = session_name)
 
       progress.echo("Starting session " + session_name + " ...")
       Isabelle_Process.start(
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Pure/Tools/profiling.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -84,8 +84,7 @@
         Isabelle_System.with_tmp_dir("profiling") { dir =>
           val putenv = List("ISABELLE_PROFILING" -> dir.implode)
           File.write(dir + Path.explode("args.yxml"), YXML.string_of_body(encode_args(args)))
-          val session_heaps =
-            ML_Process.session_heaps(store, session_background, logic = session_name)
+          val session_heaps = store.session_heaps(session_background, logic = session_name)
           ML_Process(store.options, session_background, session_heaps, args = eval_args,
             env = Isabelle_System.Settings.env(putenv)).result().check
           decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -294,7 +294,7 @@
     for ((session_background, session) <- try_session) {
       val store = Store(options)
       val session_heaps =
-        ML_Process.session_heaps(store, session_background, logic = session_background.session_name)
+        store.session_heaps(session_background, logic = session_background.session_name)
 
       session_.change(_ => Some(session))
 
diff -r 84534cc9c97e -r 20ffc02d0b0e src/Tools/jEdit/src/jedit_session.scala
--- a/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 21:58:20 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_session.scala	Tue Jun 24 22:08:20 2025 +0200
@@ -162,8 +162,7 @@
     val session = PIDE.session
     val session_background = PIDE.resources.session_background
     val session_heaps =
-      ML_Process.session_heaps(session.store, session_background,
-        logic = session_background.session_name)
+      session.store.session_heaps(session_background, logic = session_background.session_name)
 
     session.phase_changed += PIDE.plugin.session_phase_changed