clarified modules;
authorwenzelm
Thu, 02 Mar 2023 11:36:10 +0100
changeset 77472 a073ac3f3b56
parent 77471 50488bcd99f6
child 77473 362bf802013e
clarified modules;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build_process.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 02 11:25:50 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 02 11:36:10 2023 +0100
@@ -1508,6 +1508,11 @@
       (relevant, ok)
     }
 
+    def init_output(name: String): Unit = {
+      clean_output(name)
+      using(open_database(name, output = true))(init_session_info(_, name))
+    }
+
     def check_output(
       name: String,
       sources_shasum: SHA1.Shasum,
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 11:25:50 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 11:36:10 2023 +0100
@@ -596,9 +596,7 @@
     else {
       progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...")
 
-      store.clean_output(session_name)
-      using(store.open_database(session_name, output = true))(
-        store.init_session_info(_, session_name))
+      store.init_output(session_name)
 
       val session_background = build_deps.background(session_name)
       val session_heaps =