# HG changeset patch # User wenzelm # Date 1708178928 -3600 # Node ID 51e9d1a80e39387c762fd013ab6333e94e5de8fb # Parent 1b0668acf319e1e9158f33bbd99efea4f84b5eb3 clarified signature; diff -r 1b0668acf319 -r 51e9d1a80e39 src/Pure/Build/build.scala --- a/src/Pure/Build/build.scala Sat Feb 17 15:04:53 2024 +0100 +++ b/src/Pure/Build/build.scala Sat Feb 17 15:08:48 2024 +0100 @@ -27,7 +27,7 @@ sealed case class Context( store: Store, - build_deps: isabelle.Sessions.Deps, + deps: isabelle.Sessions.Deps, engine: Engine = Engine.Default, afp_root: Option[Path] = None, build_hosts: List[Build_Cluster.Host] = Nil, @@ -47,7 +47,7 @@ def build_options: Options = store.options - def sessions_structure: isabelle.Sessions.Structure = build_deps.sessions_structure + def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure def jobs: Int = max_jobs.getOrElse(1) def worker_active: Boolean = jobs > 0 @@ -62,7 +62,7 @@ results: Map[String, Process_Result] = Map.empty, other_rc: Int = Process_Result.RC.ok ): Results = { - new Results(context.store, context.build_deps, results, other_rc) + new Results(context.store, context.deps, results, other_rc) } } diff -r 1b0668acf319 -r 51e9d1a80e39 src/Pure/Build/build_process.scala --- a/src/Pure/Build/build_process.scala Sat Feb 17 15:04:53 2024 +0100 +++ b/src/Pure/Build/build_process.scala Sat Feb 17 15:08:48 2024 +0100 @@ -117,7 +117,7 @@ val deps = info.parent.toList val prefs = info.session_prefs val ancestors = sessions_structure.build_requirements(deps) - val sources_shasum = build_context.build_deps.sources_shasum(name) + val sources_shasum = build_context.deps.sources_shasum(name) if (graph0.defined(name)) { val session0 = graph0.get_node(name) @@ -846,7 +846,7 @@ protected final val store: Store = build_context.store protected final val build_options: Options = store.options - protected final val build_deps: isabelle.Sessions.Deps = build_context.build_deps + protected final val build_deps: isabelle.Sessions.Deps = build_context.deps protected final val hostname: String = build_context.hostname protected final val build_uuid: String = build_context.build_uuid