--- a/etc/build.props Wed Feb 14 11:08:05 2024 +0100
+++ b/etc/build.props Wed Feb 14 14:16:56 2024 +0100
@@ -68,6 +68,7 @@
src/Pure/Concurrent/future.scala \
src/Pure/Concurrent/isabelle_thread.scala \
src/Pure/Concurrent/mailbox.scala \
+ src/Pure/Concurrent/multithreading.scala \
src/Pure/Concurrent/par_list.scala \
src/Pure/Concurrent/synchronized.scala \
src/Pure/GUI/color_value.scala \
--- a/src/HOL/Tools/Nitpick/kodkod.scala Wed Feb 14 11:08:05 2024 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Wed Feb 14 14:16:56 2024 +0100
@@ -42,7 +42,7 @@
): Result = {
/* executor */
- val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
+ val pool_size = if (max_threads == 0) Multithreading.max_threads() else max_threads
val executor: ThreadPoolExecutor =
new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
--- a/src/Pure/Concurrent/isabelle_thread.scala Wed Feb 14 11:08:05 2024 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Wed Feb 14 14:16:56 2024 +0100
@@ -72,13 +72,8 @@
/* thread pool */
- def max_threads(): Int = {
- val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
- if (m > 0) m else (Host.num_cpus() max 1) min 8
- }
-
lazy val pool: ThreadPoolExecutor = {
- val n = max_threads()
+ val n = Multithreading.max_threads()
val executor =
new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
executor.setThreadFactory(
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/multithreading.scala Wed Feb 14 14:16:56 2024 +0100
@@ -0,0 +1,17 @@
+/* Title: Pure/Concurrent/multithreading.scala
+ Author: Makarius
+
+Multithreading in Isabelle/Scala.
+*/
+
+package isabelle
+
+
+object Multithreading {
+ /* max_threads */
+
+ def max_threads(): Int = {
+ val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+ if (m > 0) m else (Host.num_cpus() max 1) min 8
+ }
+}