# 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