# HG changeset patch
# User wenzelm
# Date 1689929771 -7200
# Node ID fd24f380b588af601eee688b9efc202fac4a449e
# Parent  c157af5f346e6734acafa1d95185ec14dd3dca05
clarified modules;

diff -r c157af5f346e -r fd24f380b588 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Jul 20 12:55:47 2023 +0200
+++ b/src/Pure/Tools/build.scala	Fri Jul 21 10:56:11 2023 +0200
@@ -23,10 +23,39 @@
 
 
 
+  /* context */
+
+  sealed case class Context(
+    store: Store,
+    build_deps: isabelle.Sessions.Deps,
+    afp_root: Option[Path] = None,
+    build_hosts: List[Build_Cluster.Host] = Nil,
+    ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
+    hostname: String = Isabelle_System.hostname(),
+    numa_shuffling: Boolean = false,
+    build_heap: Boolean = false,
+    max_jobs: Int = 1,
+    fresh_build: Boolean = false,
+    no_build: Boolean = false,
+    session_setup: (String, Session) => Unit = (_, _) => (),
+    build_uuid: String = UUID.random().toString,
+    master: Boolean = false
+  ) {
+    override def toString: String =
+      "Build.Context(build_uuid = " + quote(build_uuid) + if_proper(master, ", master = true") + ")"
+
+    def build_options: Options = store.options
+
+    def sessions_structure: isabelle.Sessions.Structure = build_deps.sessions_structure
+
+    def worker_active: Boolean = max_jobs > 0
+  }
+
+
   /* results */
 
   object Results {
-    def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results =
+    def apply(context: Context, results: Map[String, Process_Result]): Results =
       new Results(context.store, context.build_deps, results)
   }
 
@@ -86,13 +115,13 @@
     }
 
     def build_process(
-      build_context: Build_Process.Context,
+      build_context: Context,
       build_progress: Progress,
       server: SSH.Server
     ): Build_Process = new Build_Process(build_context, build_progress, server)
 
     final def run_process(
-      context: Build_Process.Context,
+      context: Context,
       progress: Progress,
       server: SSH.Server
     ): Results = {
@@ -197,7 +226,7 @@
         /* build process and results */
 
         val build_context =
-          Build_Process.Context(store, build_deps, afp_root = afp_root, build_hosts = build_hosts,
+          Context(store, build_deps, afp_root = afp_root, build_hosts = build_hosts,
             hostname = hostname(build_options), build_heap = build_heap,
             numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
             no_build = no_build, session_setup = session_setup, master = true)
@@ -494,7 +523,7 @@
             Sessions.deps(sessions_structure, progress = progress, inlined_files = true).check_errors
 
           val build_context =
-            Build_Process.Context(store, build_deps, afp_root = afp_root,
+            Context(store, build_deps, afp_root = afp_root,
               hostname = hostname(build_options), numa_shuffling = numa_shuffling,
               max_jobs = max_jobs, build_uuid = build_master.build_uuid)
 
diff -r c157af5f346e -r fd24f380b588 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Thu Jul 20 12:55:47 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Fri Jul 21 10:56:11 2023 +0200
@@ -110,7 +110,7 @@
 
 // class extensible via Build.Engine.build_process() and Build_Process.init_cluster()
 class Build_Cluster(
-  build_context: Build_Process.Context,
+  build_context: Build.Context,
   remote_hosts: List[Build_Cluster.Host],
   progress: Progress = new Progress
 ) extends AutoCloseable {
diff -r c157af5f346e -r fd24f380b588 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Jul 20 12:55:47 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Jul 21 10:56:11 2023 +0200
@@ -20,7 +20,7 @@
   /* build session */
 
   def start_session(
-    build_context: Build_Process.Context,
+    build_context: Build.Context,
     session_context: Session_Context,
     progress: Progress,
     log: Logger,
@@ -98,7 +98,7 @@
   ) extends Library.Named
 
   class Session_Job private[Build_Job](
-    build_context: Build_Process.Context,
+    build_context: Build.Context,
     session_context: Session_Context,
     progress: Progress,
     log: Logger,
diff -r c157af5f346e -r fd24f380b588 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Jul 20 12:55:47 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jul 21 10:56:11 2023 +0200
@@ -14,38 +14,7 @@
 
 
 object Build_Process {
-  /** static context **/
-
-  sealed case class Context(
-    store: Store,
-    build_deps: isabelle.Sessions.Deps,
-    afp_root: Option[Path] = None,
-    build_hosts: List[Build_Cluster.Host] = Nil,
-    ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
-    hostname: String = Isabelle_System.hostname(),
-    numa_shuffling: Boolean = false,
-    build_heap: Boolean = false,
-    max_jobs: Int = 1,
-    fresh_build: Boolean = false,
-    no_build: Boolean = false,
-    session_setup: (String, Session) => Unit = (_, _) => (),
-    build_uuid: String = UUID.random().toString,
-    master: Boolean = false
-  ) {
-    override def toString: String =
-      "Build_Process.Context(build_uuid = " + quote(build_uuid) +
-        if_proper(master, ", master = true") + ")"
-
-    def build_options: Options = store.options
-
-    def sessions_structure: isabelle.Sessions.Structure = build_deps.sessions_structure
-
-    def worker_active: Boolean = max_jobs > 0
-  }
-
-
-
-  /** dynamic state **/
+  /** state vs. database **/
 
   sealed case class Build(
     build_uuid: String,   // Database_Progress.context_uuid
@@ -131,7 +100,7 @@
     }
 
     def init(
-      build_context: Context,
+      build_context: isabelle.Build.Context,
       database_server: Option[SQL.Database],
       progress: Progress = new Progress
     ): Sessions = {
@@ -840,7 +809,7 @@
 /** main process **/
 
 class Build_Process(
-  protected final val build_context: Build_Process.Context,
+  protected final val build_context: Build.Context,
   protected final val build_progress: Progress,
   protected final val server: SSH.Server
 )