diff -r ce47945ce4fb -r f1bdf10f95d8 src/Pure/Concurrent/multithreading.ML --- a/src/Pure/Concurrent/multithreading.ML Sat Apr 09 14:11:31 2016 +0200 +++ b/src/Pure/Concurrent/multithreading.ML Sat Apr 09 14:17:50 2016 +0200 @@ -6,7 +6,7 @@ signature MULTITHREADING = sig - val max_threads_value: unit -> int + val max_threads: unit -> int val max_threads_update: int -> unit val enabled: unit -> bool val sync_wait: Thread.threadAttribute list option -> Time.time option -> @@ -21,7 +21,9 @@ structure Multithreading: MULTITHREADING = struct -(* options *) +(* max_threads *) + +local fun num_processors () = (case Thread.numPhysicalProcessors () of @@ -31,11 +33,15 @@ fun max_threads_result m = if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8); -val max_threads = ref 1; -fun max_threads_value () = ! max_threads; -fun max_threads_update m = max_threads := max_threads_result m; +val max_threads_state = ref 1; + +in -fun enabled () = max_threads_value () > 1; +fun max_threads () = ! max_threads_state; +fun max_threads_update m = max_threads_state := max_threads_result m; +fun enabled () = max_threads () > 1; + +end; (* synchronous wait *)