virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
authorwenzelm
Sat, 09 Apr 2016 14:21:29 +0200
changeset 62926 9ff9bcbc2341
parent 62925 f1bdf10f95d8
child 62927 bb2b8e915243
virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:17:50 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:21:29 2016 +0200
@@ -31,7 +31,9 @@
   | NONE => Thread.numProcessors ());
 
 fun max_threads_result m =
-  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
+  if Thread_Data.is_virtual then 1
+  else if m > 0 then m
+  else Int.min (Int.max (num_processors (), 1), 8);
 
 val max_threads_state = ref 1;