# HG changeset patch
# User wenzelm
# Date 1677694399 -3600
# Node ID e72b1f5fd88df2eb34407b5e4874a104cb75b753
# Parent  9016252f9470e97e142a9d9d0457f43fbf39e9e3
tuned signature;

diff -r 9016252f9470 -r e72b1f5fd88d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 01 16:01:01 2023 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 01 19:13:19 2023 +0100
@@ -13,7 +13,7 @@
 
   object Results {
     def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results =
-      new Results(context.store, context.deps, results)
+      new Results(context.store, context.build_deps, results)
   }
 
   class Results private(
diff -r 9016252f9470 -r e72b1f5fd88d src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 16:01:01 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 19:13:19 2023 +0100
@@ -18,7 +18,7 @@
   object Context {
     def apply(
       store: Sessions.Store,
-      deps: Sessions.Deps,
+      build_deps: Sessions.Deps,
       progress: Progress = new Progress,
       hostname: String = Isabelle_System.hostname(),
       numa_shuffling: Boolean = false,
@@ -30,7 +30,7 @@
       session_setup: (String, Session) => Unit = (_, _) => (),
       instance: String = UUID.random().toString
     ): Context = {
-      val sessions_structure = deps.sessions_structure
+      val sessions_structure = build_deps.sessions_structure
       val build_graph = sessions_structure.build_graph
 
       val sessions =
@@ -78,7 +78,7 @@
         }
 
       val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
-      new Context(instance, store, deps, sessions, ordering, progress, hostname, numa_nodes,
+      new Context(instance, store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
         no_build = no_build, verbose = verbose, session_setup)
     }
@@ -87,7 +87,7 @@
   final class Context private(
     val instance: String,
     val store: Sessions.Store,
-    val deps: Sessions.Deps,
+    val build_deps: Sessions.Deps,
     val sessions: Map[String, Build_Job.Session_Context],
     val ordering: Ordering[String],
     val progress: Progress,
@@ -100,7 +100,7 @@
     val verbose: Boolean,
     val session_setup: (String, Session) => Unit,
   ) {
-    def sessions_structure: Sessions.Structure = deps.sessions_structure
+    def sessions_structure: Sessions.Structure = build_deps.sessions_structure
 
     def session_context(session: String): Build_Job.Session_Context = sessions(session)
 
@@ -480,7 +480,7 @@
 
   protected val store: Sessions.Store = build_context.store
   protected val build_options: Options = store.options
-  protected val build_deps: Sessions.Deps = build_context.deps
+  protected val build_deps: Sessions.Deps = build_context.build_deps
   protected val progress: Progress = build_context.progress
   protected val verbose: Boolean = build_context.verbose