# HG changeset patch
# User wenzelm
# Date 1224594078 -7200
# Node ID 605a3b1ef6ba0875dc52f294f9d2ddb41ba73c20
# Parent  e2ae4a6cf1664adeda4898c07382e9fc0bcf27d1
added Future.enabled check;

diff -r e2ae4a6cf166 -r 605a3b1ef6ba src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Oct 21 15:01:16 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Oct 21 15:01:18 2008 +0200
@@ -27,6 +27,7 @@
 
 signature FUTURE =
 sig
+  val enabled: unit -> bool
   type task = TaskQueue.task
   type group = TaskQueue.group
   val thread_data: unit -> (string * task * group) option
@@ -51,6 +52,11 @@
 
 (** future values **)
 
+fun enabled () =
+  ! future_scheduler andalso Multithreading.enabled () andalso
+    not (Multithreading.self_critical ());
+
+
 (* identifiers *)
 
 type task = TaskQueue.task;
diff -r e2ae4a6cf166 -r 605a3b1ef6ba src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:16 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:18 2008 +0200
@@ -28,7 +28,7 @@
 struct
 
 fun raw_map f xs =
-  if ! future_scheduler andalso Multithreading.enabled () then
+  if Future.enabled () then
     let
       val group = TaskQueue.new_group ();
       val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
diff -r e2ae4a6cf166 -r 605a3b1ef6ba src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 21 15:01:16 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 21 15:01:18 2008 +0200
@@ -723,7 +723,7 @@
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
-    val immediate = not (! future_scheduler andalso Multithreading.enabled ());
+    val immediate = not (Future.enabled ());
     val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
     val _ =
       (case end_state of