# HG changeset patch
# User wenzelm
# Date 1677763337 -3600
# Node ID 3bc611c80346b6e40d2d41749a6c31f156c43649
# Parent  5ecaf881b5634d5d0858c240a4a7ec961b2a5a06
clarified modules;

diff -r 5ecaf881b563 -r 3bc611c80346 etc/build.props
--- a/etc/build.props	Thu Mar 02 13:26:46 2023 +0100
+++ b/etc/build.props	Thu Mar 02 14:22:17 2023 +0100
@@ -152,6 +152,7 @@
   src/Pure/System/components.scala \
   src/Pure/System/executable.scala \
   src/Pure/System/getopts.scala \
+  src/Pure/System/host.scala \
   src/Pure/System/isabelle_charset.scala \
   src/Pure/System/isabelle_fonts.scala \
   src/Pure/System/isabelle_platform.scala \
diff -r 5ecaf881b563 -r 3bc611c80346 src/Pure/System/host.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/host.scala	Thu Mar 02 14:22:17 2023 +0100
@@ -0,0 +1,16 @@
+/*  Title:      Pure/System/host.scala
+    Author:     Makarius
+
+Information about compute hosts.
+*/
+
+package isabelle
+
+
+object Host {
+  /* allocated resources */
+
+  object Node_Info { def none: Node_Info = Node_Info("", None) }
+
+  sealed case class Node_Info(hostname: String, numa_node: Option[Int])
+}
diff -r 5ecaf881b563 -r 3bc611c80346 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Mar 02 13:26:46 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Mar 02 14:22:17 2023 +0100
@@ -13,7 +13,7 @@
 
 trait Build_Job {
   def job_name: String
-  def node_info: Build_Job.Node_Info
+  def node_info: Host.Node_Info
   def terminate(): Unit = ()
   def is_finished: Boolean = false
   def finish: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
@@ -21,16 +21,13 @@
 }
 
 object Build_Job {
-  object Node_Info { def none: Node_Info = Node_Info("", None) }
-  sealed case class Node_Info(hostname: String, numa_node: Option[Int])
-
-  sealed case class Result(node_info: Node_Info, process_result: Process_Result) {
+  sealed case class Result(node_info: Host.Node_Info, process_result: Process_Result) {
     def ok: Boolean = process_result.ok
   }
 
   sealed case class Abstract(
     override val job_name: String,
-    override val node_info: Node_Info
+    override val node_info: Host.Node_Info
   ) extends Build_Job {
     override def make_abstract: Abstract = this
   }
@@ -44,7 +41,7 @@
     build_context: Build_Process.Context,
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
-    node_info: Node_Info
+    node_info: Host.Node_Info
   ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info)
 
   object Session_Context {
@@ -105,7 +102,7 @@
     build_context: Build_Process.Context,
     session_background: Sessions.Background,
     input_shasum: SHA1.Shasum,
-    override val node_info: Node_Info
+    override val node_info: Host.Node_Info
   ) extends Build_Job {
     private val store = build_context.store
     private val progress = build_context.progress
diff -r 5ecaf881b563 -r 3bc611c80346 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Mar 02 13:26:46 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Thu Mar 02 14:22:17 2023 +0100
@@ -139,7 +139,7 @@
   case class Result(
     process_result: Process_Result,
     output_shasum: SHA1.Shasum,
-    node_info: Build_Job.Node_Info,
+    node_info: Host.Node_Info,
     current: Boolean
   ) {
     def ok: Boolean = process_result.ok
@@ -188,7 +188,7 @@
       name: String,
       process_result: Process_Result,
       output_shasum: SHA1.Shasum,
-      node_info: Build_Job.Node_Info = Build_Job.Node_Info.none,
+      node_info: Host.Node_Info = Host.Node_Info.none,
       current: Boolean = false
     ): State = {
       val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current)
@@ -347,7 +347,7 @@
             val name = res.string(Running.name)
             val hostname = res.string(Running.hostname)
             val numa_node = res.get_int(Running.numa_node)
-            Build_Job.Abstract(name, Build_Job.Node_Info(hostname, numa_node))
+            Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node))
           })
       }
 
@@ -389,7 +389,7 @@
             val timing_elapsed = res.long(Results.timing_elapsed)
             val timing_cpu = res.long(Results.timing_cpu)
             val timing_gc = res.long(Results.timing_gc)
-            val node_info = Build_Job.Node_Info(hostname, numa_node)
+            val node_info = Host.Node_Info(hostname, numa_node)
             val process_result =
               Process_Result(rc,
                 out_lines = split_lines(out),
@@ -599,7 +599,7 @@
       store.init_output(session_name)
 
       val (numa_node, state1) = state.numa_next(build_context.numa_nodes)
-      val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
+      val node_info = Host.Node_Info(build_context.hostname, numa_node)
       val job =
         Build_Job.start_session(
           build_context, build_deps.background(session_name), input_shasum, node_info)