--- 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
--- 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
--- 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,
--- 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
--- 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] = {
--- 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 =
--- 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(
--- 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(
--- 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"))))
--- 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))
--- 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