1.1 --- a/src/Pure/Concurrent/future.ML	Fri Aug 19 17:05:10 2011 +0900
     1.2 +++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 12:03:44 2011 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4    val join_results: 'a future list -> 'a Exn.result list
     1.5    val join_result: 'a future -> 'a Exn.result
     1.6    val join: 'a future -> 'a
     1.7 +  val value_result: 'a Exn.result -> 'a future
     1.8    val value: 'a -> 'a future
     1.9    val map: ('a -> 'b) -> 'a future -> 'b future
    1.10    val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    1.11 @@ -524,14 +525,16 @@
    1.12  
    1.13  (* fast-path versions -- bypassing task queue *)
    1.14  
    1.15 -fun value (x: 'a) =
    1.16 +fun value_result (res: 'a Exn.result) =
    1.17    let
    1.18      val task = Task_Queue.dummy_task ();
    1.19      val group = Task_Queue.group_of_task task;
    1.20      val result = Single_Assignment.var "value" : 'a result;
    1.21 -    val _ = assign_result group result (Exn.Res x);
    1.22 +    val _ = assign_result group result res;
    1.23    in Future {promised = false, task = task, result = result} end;
    1.24  
    1.25 +fun value x = value_result (Exn.Res x);
    1.26 +
    1.27  fun map_future f x =
    1.28    let
    1.29      val task = task_of x;
    1.30 @@ -553,7 +556,7 @@
    1.31  
    1.32  fun cond_forks args es =
    1.33    if Multithreading.enabled () then forks args es
    1.34 -  else map (fn e => value (e ())) es;
    1.35 +  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    1.36  
    1.37  
    1.38  (* promised futures -- fulfilled by external means *)