clarified modules: centralize default policy;

--- a/src/Pure/Build/build_schedule.scala	Sat Feb 17 17:12:37 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Feb 17 17:23:22 2024 +0100
@@ -316,6 +316,10 @@
   case class Host(info: isabelle.Host.Info, build: Build_Cluster.Host) {
     def name: String = info.hostname
     def num_cpus: Int = info.num_cpus
+    def max_threads(options: Options): Int =
+      Multithreading.max_threads(
+        value = (options ++ build.options).int("threads"),
+        default = num_cpus)
   }
 
   object Host_Infos {
@@ -610,13 +614,8 @@
   class Default_Heuristic(host_infos: Host_Infos, options: Options) extends Priority_Rule {
     override def toString: String = "default heuristic"
 
-    def host_threads(host: Host): Int = {
-      val m = (options ++ host.build.options).int("threads")
-      if (m > 0) m else (host.num_cpus max 1) min 8
-    }
-
     def next_jobs(resources: Resources, sorted_jobs: List[String], host: Host): List[Config] =
-      sorted_jobs.zip(resources.unused_nodes(host, host_threads(host))).map(Config(_, _))
+      sorted_jobs.zip(resources.unused_nodes(host, host.max_threads(options))).map(Config(_, _))
 
     def select_next(state: Build_Process.State): List[Config] = {
       val sorted_jobs = state.next_ready.sortBy(_.name)(state.sessions.ordering).map(_.name)

--- a/src/Pure/Concurrent/multithreading.scala	Sat Feb 17 17:12:37 2024 +0100
+++ b/src/Pure/Concurrent/multithreading.scala	Sat Feb 17 17:23:22 2024 +0100
@@ -42,8 +42,10 @@
 
   /* max_threads */
 
-  def max_threads(): Int = {
-    val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-    if (m > 0) m else num_processors() min 8
+  def max_threads(
+    value: Int = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0,
+    default: => Int = num_processors()
+  ): Int = {
+    if (value > 0) value else (default max 1) min 8
   }
 }