# 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 *)