clarified signature: more explicit types/scopes;
authorwenzelm
Sat, 17 Feb 2024 21:21:00 +0100
changeset 79655 422a6e04cf0f
parent 79654 59debf50c9f7
child 79656 10e560f2f580
clarified signature: more explicit types/scopes;
src/Pure/Build/build_schedule.scala
src/Pure/System/options.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 {
--- 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 */