# HG changeset patch
# User wenzelm
# Date 1421249013 -3600
# Node ID b5d43b01a6b365149a2ed5a59d4b48c2b252c44b
# Parent  3b5da177ae6b74987c351065db7e5921bcc36ce4
added Promise.cancel;

diff -r 3b5da177ae6b -r b5d43b01a6b3 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Wed Jan 14 14:28:52 2015 +0100
+++ b/src/Pure/Concurrent/future.scala	Wed Jan 14 16:23:33 2015 +0100
@@ -47,6 +47,7 @@
 
 trait Promise[A] extends Future[A]
 {
+  def cancel: Unit
   def fulfill_result(res: Exn.Result[A]): Unit
   def fulfill(x: A): Unit
 }
@@ -78,6 +79,10 @@
 {
   override def is_finished: Boolean = promise.isCompleted
 
+  def cancel: Unit =
+    try { fulfill_result(Exn.Exn(Exn.Interrupt())) }
+    catch { case _: IllegalStateException => }
+
   def fulfill_result(res: Exn.Result[A]): Unit =
     res match {
       case Exn.Res(x) => promise.success(x)