# HG changeset patch
# User wenzelm
# Date 1453900198 -3600
# Node ID ec35b8aca63694539bcfb3d42a6cf580f151c7c2
# Parent  d9410066dbd5c3b87e987dc434eddd52b40fd811
proper try_run for exactly one evaluation of body (amending 91c3aedbfc5e);

diff -r d9410066dbd5 -r ec35b8aca636 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Mon Jan 25 14:51:04 2016 +0100
+++ b/src/Pure/Concurrent/future.scala	Wed Jan 27 14:09:58 2016 +0100
@@ -88,7 +88,7 @@
       status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
     }
   }
-  private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body })
+  private val task = Standard_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
 
   def join_result: Exn.Result[A] =
   {