# HG changeset patch # User wenzelm # Date 1350641293 -7200 # Node ID d1ecb3554b2546b83657360588290cecbcd78b9a # Parent 6f7985a42889c515657ad856ab3f20347c70453e clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.); diff -r 6f7985a42889 -r d1ecb3554b25 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Oct 18 20:59:46 2012 +0200 +++ b/src/Pure/Concurrent/future.ML Fri Oct 19 12:08:13 2012 +0200 @@ -497,8 +497,6 @@ (* join *) -local - fun get_result x = (case peek x of NONE => Exn.Exn (Fail "Unfinished future") @@ -509,6 +507,8 @@ | SOME exn => Exn.Exn exn) else res); +local + fun join_next deps = (*requires SYNCHRONIZED*) if null deps then NONE else @@ -561,23 +561,25 @@ else map (fn e => value_result (Exn.interruptible_capture e ())) es; fun map_future f x = - let - val task = task_of x; - val group = Task_Queue.group_of_task task; - val (result, job) = future_job group true (fn () => f (join x)); + if is_finished x then value (f (join x)) + else + let + val task = task_of x; + val group = Task_Queue.group_of_task task; + val (result, job) = future_job group true (fn () => f (join x)); - val extended = SYNCHRONIZED "extend" (fn () => - (case Task_Queue.extend task job (! queue) of - SOME queue' => (queue := queue'; true) - | NONE => false)); - in - if extended then Future {promised = false, task = task, result = result} - else - (singleton o cond_forks) - {name = "map_future", group = SOME group, deps = [task], - pri = Task_Queue.pri_of_task task, interrupts = true} - (fn () => f (join x)) - end; + val extended = SYNCHRONIZED "extend" (fn () => + (case Task_Queue.extend task job (! queue) of + SOME queue' => (queue := queue'; true) + | NONE => false)); + in + if extended then Future {promised = false, task = task, result = result} + else + (singleton o cond_forks) + {name = "map_future", group = SOME group, deps = [task], + pri = Task_Queue.pri_of_task task, interrupts = true} + (fn () => f (join x)) + end; (* promised futures -- fulfilled by external means *)