# HG changeset patch
# User wenzelm
# Date 1313748224 -7200
# Node ID a0ddd57604442369170df74b7a1c6ceaeae5fcb4
# Parent  83c4f8ba0aa328114a1bc0dd2b72a68bf838de33
clarified Future.cond_forks: more uniform handling of exceptional situations;

diff -r 83c4f8ba0aa3 -r a0ddd5760444 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 17:05:10 2011 +0900
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 12:03:44 2011 +0200
@@ -58,6 +58,7 @@
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
+  val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
   val map: ('a -> 'b) -> 'a future -> 'b future
   val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
@@ -524,14 +525,16 @@
 
 (* fast-path versions -- bypassing task queue *)
 
-fun value (x: 'a) =
+fun value_result (res: 'a Exn.result) =
   let
     val task = Task_Queue.dummy_task ();
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
-    val _ = assign_result group result (Exn.Res x);
+    val _ = assign_result group result res;
   in Future {promised = false, task = task, result = result} end;
 
+fun value x = value_result (Exn.Res x);
+
 fun map_future f x =
   let
     val task = task_of x;
@@ -553,7 +556,7 @@
 
 fun cond_forks args es =
   if Multithreading.enabled () then forks args es
-  else map (fn e => value (e ())) es;
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 
 (* promised futures -- fulfilled by external means *)