clarified: more operations;

--- a/src/Pure/Build/build_schedule.scala	Sun Mar 17 19:45:07 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sun Mar 17 19:53:31 2024 +0100
@@ -334,6 +334,24 @@
 
   /* host information */
 
+  object Host {
+    def load(build_host: Build_Cluster.Host, host_db: SQL.Database): Host = {
+      val name = build_host.name
+      val info =
+        isabelle.Host.read_info(host_db, name).getOrElse(error("No info for host " + quote(name)))
+      val score = info.benchmark_score.getOrElse(error("No benchmark for " + quote(name)))
+
+      Host(
+        name = name,
+        num_cpus = info.num_cpus,
+        max_jobs = build_host.jobs,
+        numa = build_host.numa,
+        numa_nodes = info.numa_nodes,
+        benchmark_score = score,
+        options = build_host.options)
+    }
+  }
+
   case class Host(
     name: String,
     num_cpus: Int,
@@ -347,25 +365,8 @@
   }
 
   object Host_Infos {
-    def load(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = {
-      def get_host(build_host: Build_Cluster.Host): Host = {
-        val name = build_host.name
-        val info =
-          isabelle.Host.read_info(db, name).getOrElse(error("No info for host " + quote(name)))
-        val score = info.benchmark_score.getOrElse(error("No benchmark for " + quote(name)))
-
-        Host(
-          name = name,
-          num_cpus = info.num_cpus,
-          max_jobs = build_host.jobs,
-          numa = build_host.numa,
-          numa_nodes = info.numa_nodes,
-          benchmark_score = score,
-          options = build_host.options)
-      }
-
-      new Host_Infos(build_hosts.map(get_host))
-    }
+    def load(build_hosts: List[Build_Cluster.Host], host_db: SQL.Database): Host_Infos =
+      new Host_Infos(build_hosts.map(Host.load(_, host_db)))
   }
 
   class Host_Infos private(val hosts: List[Host]) {