clarified signature;
authorwenzelm
Tue, 27 Jun 2023 11:39:02 +0200
changeset 78215 cfd58705fbaf
parent 78214 edf86c709535
child 78216 13edc16bc14c
clarified signature;
src/Pure/Thy/store.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_process.scala
--- a/src/Pure/Thy/store.scala	Tue Jun 27 11:17:52 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 27 11:39:02 2023 +0200
@@ -302,8 +302,6 @@
   def open_database(name: String, output: Boolean = false): SQL.Database =
     try_open_database(name, output = output) getOrElse error_database(name)
 
-  def prepare_output(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
-
   def clean_output(
     database_server: Option[SQL.Database],
     name: String,
--- a/src/Pure/Tools/build.scala	Tue Jun 27 11:17:52 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Jun 27 11:39:02 2023 +0200
@@ -168,8 +168,7 @@
         numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
         no_build = no_build, session_setup = session_setup, master = true)
 
-    store.prepare_output()
-    build_context.prepare_database()
+    build_context.store_init()
 
     if (clean_build) {
       using_optional(store.maybe_open_database_server()) { database_server =>
--- a/src/Pure/Tools/build_process.scala	Tue Jun 27 11:17:52 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Tue Jun 27 11:39:02 2023 +0200
@@ -121,7 +121,9 @@
         case None => Nil
       }
 
-    def prepare_database(): Unit = {
+    def store_init(): Unit = {
+      Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
+
       using_option(store.maybe_open_build_database(Data.database)) { db =>
         val shared_db = db.is_postgresql
         Data.transaction_lock(db, create = true) {