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