# HG changeset patch # User wenzelm # Date 1362500741 -3600 # Node ID 877edf1fc5dd3469d7448ccf2df6379f9e22888e # Parent ae707530c35955d698c5d8164f572a1f8db40dd9# Parent ef494f2288cf780327b7319fcefb1e0e9e4af4e2 merged diff -r ae707530c359 -r 877edf1fc5dd src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Tue Mar 05 17:18:02 2013 +0100 +++ b/src/Pure/Concurrent/future.ML Tue Mar 05 17:25:41 2013 +0100 @@ -70,7 +70,6 @@ val value: 'a -> 'a future val cond_forks: params -> (unit -> 'a) list -> 'a future list val map: ('a -> 'b) -> 'a future -> 'b future - val flat: 'a list future list -> 'a list future val promise_group: group -> (unit -> unit) -> 'a future val promise: (unit -> unit) -> 'a future val fulfill_result: 'a future -> 'a Exn.result -> unit @@ -608,20 +607,6 @@ (fn () => f (join x)) end; -fun flat_future futures = - (case filter_out is_finished futures of - [] => value_result (Exn.interruptible_capture (flat o joins) futures) - | [x] => map_future (fn _ => flat (joins (futures))) x - | xs => - let - val tasks = map task_of xs; - val pri = foldl1 Int.min (map Task_Queue.pri_of_task tasks); - in - (singleton o cond_forks) - {name = "flat_future", group = NONE, deps = tasks, pri = pri, interrupts = true} - (fn () => flat (joins (futures))) - end); - (* promised futures -- fulfilled by external means *) @@ -705,7 +690,6 @@ (*final declarations of this structure!*) val map = map_future; -val flat = flat_future; end;