# HG changeset patch
# User wenzelm
# Date 1314110361 -7200
# Node ID 0f0ba362ce50378ed475977ab550ce0274d451b8
# Parent  4048ca2658b78e3ebdcfe08fc8d300b18ec6f16f
discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);

diff -r 4048ca2658b7 -r 0f0ba362ce50 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 23 15:48:41 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 23 16:39:21 2011 +0200
@@ -51,7 +51,6 @@
   val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
-  val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> task list
   val cancel: 'a future -> task list
@@ -126,11 +125,6 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished future evaluation");
-
 
 
 (** scheduling **)
diff -r 4048ca2658b7 -r 0f0ba362ce50 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Tue Aug 23 15:48:41 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Tue Aug 23 16:39:21 2011 +0200
@@ -11,7 +11,6 @@
   type 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
   val is_finished: 'a lazy -> bool
-  val get_finished: 'a lazy -> 'a
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
@@ -42,11 +41,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)
 
diff -r 4048ca2658b7 -r 0f0ba362ce50 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 15:48:41 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Tue Aug 23 16:39:21 2011 +0200
@@ -27,11 +27,6 @@
 
 fun is_finished x = is_some (peek x);
 
-fun get_finished x =
-  (case peek x of
-    SOME res => Exn.release res
-  | NONE => raise Fail "Unfinished lazy evaluation");
-
 
 (* force result *)