1.1 --- a/etc/settings	Sun Jun 14 09:13:59 2009 +0200
     1.2 +++ b/etc/settings	Sun Jun 14 23:18:32 2009 +0200
     1.3 @@ -91,8 +91,7 @@
     1.4  ### Batch sessions (cf. isabelle usedir)
     1.5  ###
     1.6  
     1.7 -ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -v true -V outline=/proof,/ML"
     1.8 -#ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
     1.9 +ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
    1.10  
    1.11  # Specifically for the HOL image
    1.12  HOL_USEDIR_OPTIONS=""

     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jun 14 09:13:59 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Jun 14 23:18:32 2009 +0200
     2.3 @@ -40,9 +40,16 @@
     2.4  
     2.5  val max_threads = ref 1;
     2.6  
     2.7 +val tested_platform =
     2.8 +  let val ml_platform = getenv "ML_PLATFORM"
     2.9 +  in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
    2.10 +
    2.11  fun max_threads_value () =
    2.12 -  let val m = ! max_threads
    2.13 -  in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end;
    2.14 +  let val m = ! max_threads in
    2.15 +    if m > 0 then m
    2.16 +    else if not tested_platform then 1
    2.17 +    else Int.min (Int.max (Thread.numProcessors (), 1), 8)
    2.18 +  end;
    2.19  
    2.20  fun enabled () = max_threads_value () > 1;
    2.21