# HG changeset patch
# User wenzelm
# Date 1245056285 -7200
# Node ID 3b98fabd2cf1008331e3296a47adcfa74edd0a39
# Parent  e2272338dfcf67f2457c9109cf1a85259e404b23# Parent  fae680e3595870f499d1496eb155de461059fe40
merged

diff -r e2272338dfcf -r 3b98fabd2cf1 etc/settings
--- a/etc/settings	Mon Jun 15 09:43:30 2009 +0200
+++ b/etc/settings	Mon Jun 15 10:58:05 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 e2272338dfcf -r 3b98fabd2cf1 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jun 15 09:43:30 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Jun 15 10:58:05 2009 +0200
@@ -301,19 +301,10 @@
       val _ = scheduler_check "join check";
       val _ = Multithreading.self_critical () andalso
         error "Cannot join future values within critical section";
-
       val _ =
-        (case thread_data () of
-          NONE => List.app join_wait xs  (*alien thread -- refrain from contending for resources*)
-        | SOME (name, task) =>           (*proper task -- continue work*)
-            let
-              val pending = filter_out is_finished xs;
-              val deps = map task_of pending;
-              val _ = SYNCHRONIZED "join" (fn () =>
-                (change queue (Task_Queue.depend deps task); notify_all ()));
-              val _ = List.app join_loop pending;
-            in () end);
-
+        if is_some (thread_data ())
+        then List.app join_loop xs   (*proper task -- continue work*)
+        else List.app join_wait xs;  (*alien thread -- refrain from contending for resources*)
     in map get_result xs end) ();
 
 end;
diff -r e2272338dfcf -r 3b98fabd2cf1 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Mon Jun 15 09:43:30 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Mon Jun 15 10:58:05 2009 +0200
@@ -21,7 +21,6 @@
   val is_empty: queue -> bool
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
-  val depend: task list -> task -> queue -> queue
   val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
   val interrupt: queue -> task -> unit
   val interrupt_external: queue -> string -> unit
@@ -74,9 +73,6 @@
 fun add_job task dep (jobs: jobs) =
   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
-fun add_job_acyclic task dep (jobs: jobs) =
-  Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
-
 
 (* queue of grouped jobs *)
 
@@ -95,22 +91,25 @@
 
 (* enqueue *)
 
-fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, ...}) =
+fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) =
   let
     val task = new_task pri;
     val groups' = Inttab.cons_list (gid, task) groups;
     val jobs' = jobs
       |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
-  in (task, make_queue groups' jobs' Unknown) end;
+    val cache' =
+      (case cache of
+        Result last =>
+          if task_ord (last, task) = LESS
+          then cache else Unknown
+      | _ => Unknown);
+  in (task, make_queue groups' jobs' cache') end;
 
 fun extend task job (Queue {groups, jobs, cache}) =
   (case try (get_job jobs) task of
     SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache)
   | _ => NONE);
 
-fun depend deps task (Queue {groups, jobs, ...}) =
-  make_queue groups (fold (add_job_acyclic task) deps jobs) Unknown;
-
 
 (* dequeue *)
 
@@ -168,11 +167,14 @@
     val _ = List.app SimpleThread.interrupt running;
   in groups end;
 
-fun finish task (Queue {groups, jobs, ...}) =
+fun finish task (Queue {groups, jobs, cache}) =
   let
     val Group (gid, _) = get_group jobs task;
     val groups' = Inttab.remove_list (op =) (gid, task) groups;
     val jobs' = Task_Graph.del_node task jobs;
-  in make_queue groups' jobs' Unknown end;
+    val cache' =
+      if null (Task_Graph.imm_succs jobs task) then cache
+      else Unknown;
+  in make_queue groups' jobs' cache' end;
 
 end;
diff -r e2272338dfcf -r 3b98fabd2cf1 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jun 15 09:43:30 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Jun 15 10:58:05 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;