--- a/src/Pure/Concurrent/future.ML Wed Oct 01 12:00:00 2008 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Oct 01 12:00:01 2008 +0200
@@ -40,7 +40,6 @@
val fork_background: (unit -> 'a) -> 'a T
val join_results: 'a T list -> 'a Exn.result list
val join: 'a T -> 'a
- val release_results: 'a Exn.result list -> 'a list
val focus: task list -> unit
val interrupt_task: string -> unit
val cancel: 'a T -> unit
@@ -236,7 +235,7 @@
val result = ref (NONE: 'a Exn.result option);
val run = Multithreading.with_attributes (Thread.getAttributes ())
(fn _ => fn ok =>
- let val res = if ok then Exn.capture e () else Exn.Exn Interrupt
+ let val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt
in result := SOME res; is_some (Exn.get_result res) end);
val task = SYNCHRONIZED "future" (fn () =>
@@ -288,18 +287,6 @@
fun join x = Exn.release (singleton join_results x);
-(* release results *)
-
-fun proper_exn (Exn.Result _) = NONE
- | proper_exn (Exn.Exn Interrupt) = NONE
- | proper_exn (Exn.Exn exn) = SOME exn;
-
-fun release_results results =
- (case get_first proper_exn results of
- SOME exn => raise exn
- | NONE => List.map Exn.release results);
-
-
(* misc operations *)
(*focus: collection of high-priority task*)