1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 19 13:55:32 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 14:01:20 2011 +0200
     1.3 @@ -62,8 +62,8 @@
     1.4    val value: 'a -> 'a future
     1.5    val map: ('a -> 'b) -> 'a future -> 'b future
     1.6    val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
     1.7 -  val promise_group: Task_Queue.group -> 'a future
     1.8 -  val promise: unit -> 'a future
     1.9 +  val promise_group: Task_Queue.group -> (unit -> unit) -> 'a future
    1.10 +  val promise: (unit -> unit) -> 'a future
    1.11    val fulfill_result: 'a future -> 'a Exn.result -> unit
    1.12    val fulfill: 'a future -> 'a -> unit
    1.13    val shutdown: unit -> unit
    1.14 @@ -561,19 +561,23 @@
    1.15  
    1.16  (* promised futures -- fulfilled by external means *)
    1.17  
    1.18 -fun promise_group group : 'a future =
    1.19 +fun promise_group group abort : 'a future =
    1.20    let
    1.21      val result = Single_Assignment.var "promise" : 'a result;
    1.22 -    fun abort () = assign_result group result Exn.interrupt_exn
    1.23 +    fun assign () = assign_result group result Exn.interrupt_exn
    1.24        handle Fail _ => true
    1.25          | exn =>
    1.26 -            if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
    1.27 +            if Exn.is_interrupt exn
    1.28 +            then raise Fail "Concurrent attempt to fulfill promise"
    1.29              else reraise exn;
    1.30 +    fun job () =
    1.31 +      Multithreading.with_attributes Multithreading.no_interrupts
    1.32 +        (fn _ => assign () before abort ());
    1.33      val task = SYNCHRONIZED "enqueue_passive" (fn () =>
    1.34 -      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
    1.35 +      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
    1.36    in Future {promised = true, task = task, result = result} end;
    1.37  
    1.38 -fun promise () = promise_group (worker_subgroup ());
    1.39 +fun promise abort = promise_group (worker_subgroup ()) abort;
    1.40  
    1.41  fun fulfill_result (Future {promised, task, result}) res =
    1.42    if not promised then raise Fail "Not a promised future"