# HG changeset patch # User wenzelm # Date 1312986365 -7200 # Node ID 5d9821493bc16009983ffbe36d3596b8774347c1 # Parent 64634a9ecd466ef9e957123b64efa0ed519eddc2 tuned signature; diff -r 64634a9ecd46 -r 5d9821493bc1 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Aug 10 16:24:39 2011 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Aug 10 16:26:05 2011 +0200 @@ -39,6 +39,7 @@ val task_of: 'a future -> Task_Queue.task val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool + val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: Task_Queue.group -> unit val cancel: 'a future -> unit type fork_params = @@ -57,7 +58,6 @@ val promise: unit -> 'a future val fulfill_result: 'a future -> 'a Exn.result -> unit val fulfill: 'a future -> 'a -> unit - val interruptible_task: ('a -> 'b) -> 'a -> 'b val shutdown: unit -> unit val status: (unit -> 'a) -> 'a end;