# HG changeset patch
# User wenzelm
# Date 1248791423 -7200
# Node ID d302f1c9e356fd4aabe1cb908c2e3d485d4945b6
# Parent  8b02619c3039384bb6b049bdcf675d1f65e873cd
eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;

diff -r 8b02619c3039 -r d302f1c9e356 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Jul 28 16:28:49 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Jul 28 16:30:23 2009 +0200
@@ -27,7 +27,6 @@
 
 signature FUTURE =
 sig
-  val enabled: unit -> bool
   type task = Task_Queue.task
   type group = Task_Queue.group
   val is_worker: unit -> bool
@@ -57,11 +56,6 @@
 
 (** future values **)
 
-fun enabled () =
-  Multithreading.enabled () andalso
-    not (Multithreading.self_critical ());
-
-
 (* identifiers *)
 
 type task = Task_Queue.task;
diff -r 8b02619c3039 -r d302f1c9e356 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Jul 28 16:28:49 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 28 16:30:23 2009 +0200
@@ -27,10 +27,8 @@
 struct
 
 fun raw_map f xs =
-  if Future.enabled () then
-    let val group = Task_Queue.new_group (Future.worker_group ())
-    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
-  else map (Exn.capture f) xs;
+  let val group = Task_Queue.new_group (Future.worker_group ())
+  in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end;
 
 fun map f xs = Exn.release_first (raw_map f xs);
 
diff -r 8b02619c3039 -r d302f1c9e356 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Jul 28 16:28:49 2009 +0200
+++ b/src/Pure/goal.ML	Tue Jul 28 16:30:23 2009 +0200
@@ -103,7 +103,7 @@
 val parallel_proofs = ref 1;
 
 fun future_enabled () =
-  Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+  Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
 
 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;