clarified modules;
authorwenzelm
Thu, 02 Mar 2023 11:19:41 +0100
changeset 77470 38503d9ff2e5
parent 77469 5af7e8ffcab7
child 77471 50488bcd99f6
clarified modules;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 11:11:55 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 11:19:41 2023 +0100
@@ -101,6 +101,15 @@
     val session_setup: (String, Session) => Unit,
     val uuid: String
   ) {
+    def build_options: Options = store.options
+
+    val log: Logger =
+      build_options.string("system_log") match {
+        case "" => No_Logger
+        case "-" => Logger.make(progress)
+        case log_file => Logger.make(Some(Path.explode(log_file)))
+      }
+
     def sessions_structure: Sessions.Structure = build_deps.sessions_structure
 
     def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum
@@ -482,13 +491,6 @@
   protected val progress: Progress = build_context.progress
   protected val verbose: Boolean = build_context.verbose
 
-  protected val log: Logger =
-    build_options.string("system_log") match {
-      case "" => No_Logger
-      case "-" => Logger.make(progress)
-      case log_file => Logger.make(Some(Path.explode(log_file)))
-    }
-
 
   /* global state: internal var vs. external database */
 
@@ -606,7 +608,7 @@
         }
 
       val resources =
-        new Resources(session_background, log = log,
+        new Resources(session_background, log = build_context.log,
           command_timings = build_context.old_command_timings(session_name))
 
       val (numa_node, state1) = state.numa_next(build_context.numa_nodes)