# HG changeset patch
# User wenzelm
# Date 1245014312 -7200
# Node ID 2f8ed0dca3bd2c2a54a5d3269505ce3e42dd402f
# Parent  40d77573384820c40e51a3f0f9ba2e4851791f4b
back to default -M max, with more robust interpretation of corresponding max_threads value;

diff -r 40d775733848 -r 2f8ed0dca3bd etc/settings
--- a/etc/settings	Sun Jun 14 09:13:59 2009 +0200
+++ b/etc/settings	Sun Jun 14 23:18:32 2009 +0200
@@ -91,8 +91,7 @@
 ### Batch sessions (cf. isabelle usedir)
 ###
 
-ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -v true -V outline=/proof,/ML"
-#ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
+ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
 
 # Specifically for the HOL image
 HOL_USEDIR_OPTIONS=""
diff -r 40d775733848 -r 2f8ed0dca3bd src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jun 14 09:13:59 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jun 14 23:18:32 2009 +0200
@@ -40,9 +40,16 @@
 
 val max_threads = ref 1;
 
+val tested_platform =
+  let val ml_platform = getenv "ML_PLATFORM"
+  in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
+
 fun max_threads_value () =
-  let val m = ! max_threads
-  in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
+  let val m = ! max_threads in
+    if m > 0 then m
+    else if not tested_platform then 1
+    else Int.min (Int.max (Thread.numProcessors (), 1), 8)
+  end;
 
 fun enabled () = max_threads_value () > 1;