# HG changeset patch
# User wenzelm
# Date 1708201260 -3600
# Node ID 422a6e04cf0f975c77b2848529cf5688f44db146
# Parent  59debf50c9f7a5eb52c3d4ff0e87270c50fc353b
clarified signature: more explicit types/scopes;

diff -r 59debf50c9f7 -r 422a6e04cf0f src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Feb 17 21:18:23 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Feb 17 21:21:00 2024 +0100
@@ -316,10 +316,7 @@
   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)
+    def max_threads(options: Options): Int = (options ++ build.options).threads(default = num_cpus)
   }
 
   object Host_Infos {
diff -r 59debf50c9f7 -r 422a6e04cf0f src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Feb 17 21:18:23 2024 +0100
+++ b/src/Pure/System/options.scala	Sat Feb 17 21:21:00 2024 +0100
@@ -399,6 +399,9 @@
 
   def seconds(name: String): Time = Time.seconds(real(name))
 
+  def threads(default: => Int = Multithreading.num_processors()): Int =
+    Multithreading.max_threads(value = int("threads"), default = default)
+
 
   /* external updates */