added Future.enabled check;
authorwenzelm
Tue Oct 21 15:01:18 2008 +0200 (2008-10-21)
changeset 28645605a3b1ef6ba
parent 28644 e2ae4a6cf166
child 28646 3a8d75c935ce
added Future.enabled check;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Oct 21 15:01:16 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Oct 21 15:01:18 2008 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4  
     1.5  signature FUTURE =
     1.6  sig
     1.7 +  val enabled: unit -> bool
     1.8    type task = TaskQueue.task
     1.9    type group = TaskQueue.group
    1.10    val thread_data: unit -> (string * task * group) option
    1.11 @@ -51,6 +52,11 @@
    1.12  
    1.13  (** future values **)
    1.14  
    1.15 +fun enabled () =
    1.16 +  ! future_scheduler andalso Multithreading.enabled () andalso
    1.17 +    not (Multithreading.self_critical ());
    1.18 +
    1.19 +
    1.20  (* identifiers *)
    1.21  
    1.22  type task = TaskQueue.task;
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:16 2008 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:18 2008 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  struct
     2.5  
     2.6  fun raw_map f xs =
     2.7 -  if ! future_scheduler andalso Multithreading.enabled () then
     2.8 +  if Future.enabled () then
     2.9      let
    2.10        val group = TaskQueue.new_group ();
    2.11        val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 21 15:01:16 2008 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 21 15:01:18 2008 +0200
     3.3 @@ -723,7 +723,7 @@
     3.4    let
     3.5      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
     3.6  
     3.7 -    val immediate = not (! future_scheduler andalso Multithreading.enabled ());
     3.8 +    val immediate = not (Future.enabled ());
     3.9      val (future_results, end_state) = fold_map (unit_result immediate) input toplevel;
    3.10      val _ =
    3.11        (case end_state of