removed release_results (cf. Exn.release_all, Exn.release_first);
authorwenzelm
Wed Oct 01 12:00:01 2008 +0200 (2008-10-01)
changeset 28442bd9573735bdd
parent 28441 9b0daffc4054
child 28443 de653f1ad78b
removed release_results (cf. Exn.release_all, Exn.release_first);
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed Oct 01 12:00:00 2008 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Oct 01 12:00:01 2008 +0200
     1.3 @@ -40,7 +40,6 @@
     1.4    val fork_background: (unit -> 'a) -> 'a T
     1.5    val join_results: 'a T list -> 'a Exn.result list
     1.6    val join: 'a T -> 'a
     1.7 -  val release_results: 'a Exn.result list -> 'a list
     1.8    val focus: task list -> unit
     1.9    val interrupt_task: string -> unit
    1.10    val cancel: 'a T -> unit
    1.11 @@ -236,7 +235,7 @@
    1.12      val result = ref (NONE: 'a Exn.result option);
    1.13      val run = Multithreading.with_attributes (Thread.getAttributes ())
    1.14        (fn _ => fn ok =>
    1.15 -        let val res = if ok then Exn.capture e () else Exn.Exn Interrupt
    1.16 +        let val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt
    1.17          in result := SOME res; is_some (Exn.get_result res) end);
    1.18  
    1.19      val task = SYNCHRONIZED "future" (fn () =>
    1.20 @@ -288,18 +287,6 @@
    1.21  fun join x = Exn.release (singleton join_results x);
    1.22  
    1.23  
    1.24 -(* release results *)
    1.25 -
    1.26 -fun proper_exn (Exn.Result _) = NONE
    1.27 -  | proper_exn (Exn.Exn Interrupt) = NONE
    1.28 -  | proper_exn (Exn.Exn exn) = SOME exn;
    1.29 -
    1.30 -fun release_results results =
    1.31 -  (case get_first proper_exn results of
    1.32 -    SOME exn => raise exn
    1.33 -  | NONE => List.map Exn.release results);
    1.34 -
    1.35 -
    1.36  (* misc operations *)
    1.37  
    1.38  (*focus: collection of high-priority task*)