equal
deleted
inserted
replaced
72 |
72 |
73 /* thread pool */ |
73 /* thread pool */ |
74 |
74 |
75 def max_threads(): Int = { |
75 def max_threads(): Int = { |
76 val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
76 val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
77 if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 |
77 if (m > 0) m else (Host.num_cpus() max 1) min 8 |
78 } |
78 } |
79 |
79 |
80 lazy val pool: ThreadPoolExecutor = { |
80 lazy val pool: ThreadPoolExecutor = { |
81 val n = max_threads() |
81 val n = max_threads() |
82 val executor = |
82 val executor = |