# HG changeset patch
# User wenzelm
# Date 1677676597 -3600
# Node ID 9969b6aed223a766f0a5964ba76c11b11ad7e5c6
# Parent  7751922c66683ef7d752d17017ad864012d1f263
clarified modules (again);

diff -r 7751922c6668 -r 9969b6aed223 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 14:11:55 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 14:16:37 2023 +0100
@@ -39,6 +39,56 @@
 
   /* 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 load(
+      session: String,
+      timeout: Time,
+      store: Sessions.Store,
+      progress: Progress = new Progress
+    ): Session_Context = {
+      store.try_open_database(session) match {
+        case None => init(session, timeout = timeout)
+        case Some(db) =>
+          def ignore_error(msg: String) = {
+            progress.echo_warning(
+              "Ignoring bad database " + db + " for session " + quote(session) +
+              if_proper(msg, ":\n" + msg))
+            init(session, timeout = timeout)
+          }
+          try {
+            val command_timings = store.read_command_timings(db, session)
+            val elapsed =
+              store.read_session_timing(db, session) match {
+                case Markup.Elapsed(s) => Time.seconds(s)
+                case _ => Time.zero
+              }
+            new Session_Context(session, timeout, elapsed, command_timings)
+          }
+          catch {
+            case ERROR(msg) => ignore_error(msg)
+            case exn: java.lang.Error => ignore_error(Exn.message(exn))
+            case _: XML.Error => ignore_error("XML.Error")
+          }
+          finally { db.close() }
+      }
+    }
+  }
+
+  final class Session_Context(
+    val session: String,
+    val timeout: Time,
+    val old_time: Time,
+    val old_command_timings_blob: Bytes
+  ) {
+    def is_empty: Boolean =
+      old_time.is_zero && old_command_timings_blob.is_empty
+
+    override def toString: String = session
+  }
+
   class Build_Session(
     progress: Progress,
     verbose: Boolean,
diff -r 7751922c6668 -r 9969b6aed223 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 14:11:55 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 14:16:37 2023 +0100
@@ -15,56 +15,6 @@
 object Build_Process {
   /** static context **/
 
-  object Session_Context {
-    def init(session: String, timeout: Time = Time.zero): Session_Context =
-      new Session_Context(session, timeout, Time.zero, Bytes.empty)
-
-    def load(
-      session: String,
-      timeout: Time,
-      store: Sessions.Store,
-      progress: Progress = new Progress
-    ): Session_Context = {
-      store.try_open_database(session) match {
-        case None => init(session, timeout = timeout)
-        case Some(db) =>
-          def ignore_error(msg: String) = {
-            progress.echo_warning(
-              "Ignoring bad database " + db + " for session " + quote(session) +
-              if_proper(msg, ":\n" + msg))
-            init(session, timeout = timeout)
-          }
-          try {
-            val command_timings = store.read_command_timings(db, session)
-            val elapsed =
-              store.read_session_timing(db, session) match {
-                case Markup.Elapsed(s) => Time.seconds(s)
-                case _ => Time.zero
-              }
-            new Session_Context(session, timeout, elapsed, command_timings)
-          }
-          catch {
-            case ERROR(msg) => ignore_error(msg)
-            case exn: java.lang.Error => ignore_error(Exn.message(exn))
-            case _: XML.Error => ignore_error("XML.Error")
-          }
-          finally { db.close() }
-      }
-    }
-  }
-
-  final class Session_Context(
-    val session: String,
-    val timeout: Time,
-    val old_time: Time,
-    val old_command_timings_blob: Bytes
-  ) {
-    def is_empty: Boolean =
-      old_time.is_zero && old_command_timings_blob.is_empty
-
-    override def toString: String = session
-  }
-
   object Context {
     def apply(
       store: Sessions.Store,
@@ -88,7 +38,7 @@
           for (name <- build_graph.keys_iterator)
           yield {
             val timeout = sessions_structure(name).timeout
-            name -> Build_Process.Session_Context.load(name, timeout, store, progress = progress)
+            name -> Build_Job.Session_Context.load(name, timeout, store, progress = progress)
           })
 
       val sessions_time = {
@@ -134,7 +84,7 @@
     val instance: String,
     val store: Sessions.Store,
     val deps: Sessions.Deps,
-    sessions: Map[String, Session_Context],
+    sessions: Map[String, Build_Job.Session_Context],
     val ordering: Ordering[String],
     val progress: Progress,
     val hostname: String,
@@ -148,8 +98,8 @@
   ) {
     def sessions_structure: Sessions.Structure = deps.sessions_structure
 
-    def apply(session: String): Session_Context =
-      sessions.getOrElse(session, Session_Context.init(session))
+    def apply(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(apply(session).old_command_timings_blob, cache = store.cache)