# HG changeset patch
# User wenzelm
# Date 1199287973 -3600
# Node ID 90525e67ede76a9b0409c53cbefb7356c88bb33d
# Parent  28fac5c2af54242068c9b970486b9c9f35f78bb5
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;

diff -r 28fac5c2af54 -r 90525e67ede7 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -18,6 +18,7 @@
   val tracing: int -> (unit -> string) -> unit
   val available: bool
   val max_threads: int ref
+  val max_threads_value: unit -> int
   val self_critical: unit -> bool
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
@@ -37,6 +38,7 @@
 
 val available = false;
 val max_threads = ref (1: int);
+fun max_threads_value () = Int.max (! max_threads, 1);
 
 
 (* critical section *)
diff -r 28fac5c2af54 -r 90525e67ede7 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -38,8 +38,13 @@
   else ();
 
 val available = true;
+
 val max_threads = ref 1;
 
+fun max_threads_value () =
+  let val m = ! max_threads
+  in if m <= 0 then Thread.numProcessors () else m end;
+
 
 (* misc utils *)
 
diff -r 28fac5c2af54 -r 90525e67ede7 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:52 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Jan 02 16:32:53 2008 +0100
@@ -377,7 +377,7 @@
 in
 
 fun schedule_tasks tasks n =
-  let val m = ! Multithreading.max_threads in
+  let val m = Multithreading.max_threads_value () in
     if m <= 1 orelse n <= 1 then schedule_seq tasks
     else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);