# HG changeset patch # User wenzelm # Date 1677678440 -3600 # Node ID 0c704aba71e37f4b7cbd6a70812d47b41414f43e # Parent 3f13c6d476257f4dfc6676845d56d3c27461ae20 clarified signature: reduce explicit access to static Sessions.Structure; diff -r 3f13c6d47625 -r 0c704aba71e3 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Wed Mar 01 14:22:15 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Wed Mar 01 14:47:20 2023 +0100 @@ -40,32 +40,40 @@ /* build session */ object Session_Context { - def init(session: String, timeout: Time = Time.zero): Session_Context = - new Session_Context(session, timeout, Time.zero, Bytes.empty) + def init(name: String, + deps: List[String], + ancestors: List[String], + timeout: Time = Time.zero + ): Session_Context = new Session_Context(name, deps, ancestors, timeout, Time.zero, Bytes.empty) def load( - session: String, + name: String, + deps: List[String], + ancestors: List[String], timeout: Time, store: Sessions.Store, progress: Progress = new Progress ): Session_Context = { - store.try_open_database(session) match { - case None => init(session, timeout = timeout) + def default: Session_Context = init(name, deps, ancestors, timeout = timeout) + + store.try_open_database(name) match { + case None => default case Some(db) => def ignore_error(msg: String) = { progress.echo_warning( - "Ignoring bad database " + db + " for session " + quote(session) + + "Ignoring bad database " + db + " for session " + quote(name) + if_proper(msg, ":\n" + msg)) - init(session, timeout = timeout) + default } try { - val command_timings = store.read_command_timings(db, session) + val command_timings = store.read_command_timings(db, name) val elapsed = - store.read_session_timing(db, session) match { + store.read_session_timing(db, name) match { case Markup.Elapsed(s) => Time.seconds(s) case _ => Time.zero } - new Session_Context(session, timeout, elapsed, command_timings) + new Session_Context( + name, deps, ancestors, timeout, elapsed, command_timings) } catch { case ERROR(msg) => ignore_error(msg) @@ -78,7 +86,9 @@ } final class Session_Context( - val session: String, + val name: String, + val deps: List[String], + val ancestors: List[String], val timeout: Time, val old_time: Time, val old_command_timings_blob: Bytes @@ -86,7 +96,7 @@ def is_empty: Boolean = old_time.is_zero && old_command_timings_blob.is_empty - override def toString: String = session + override def toString: String = name } class Build_Session( diff -r 3f13c6d47625 -r 0c704aba71e3 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Wed Mar 01 14:22:15 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Wed Mar 01 14:47:20 2023 +0100 @@ -37,8 +37,13 @@ Map.from( for (name <- build_graph.keys_iterator) yield { - val timeout = sessions_structure(name).timeout - name -> Build_Job.Session_Context.load(name, timeout, store, progress = progress) + val info = sessions_structure(name) + val ancestors = + sessions_structure.build_requirements(List(name)).filterNot(_ == name) + val session_context = + Build_Job.Session_Context.load( + name, info.deps, ancestors, info.timeout, store, progress = progress) + name -> session_context }) val sessions_time = { @@ -98,11 +103,12 @@ ) { def sessions_structure: Sessions.Structure = deps.sessions_structure - def session_context(session: String): Build_Job.Session_Context = - sessions.getOrElse(session, Build_Job.Session_Context.init(session)) - def old_command_timings(session: String): List[Properties.T] = - Properties.uncompress(session_context(session).old_command_timings_blob, cache = store.cache) + sessions.get(session) match { + case Some(session_context) => + Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache) + case None => Nil + } def do_store(session: String): Boolean = build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session)