1.1 --- a/src/Pure/Concurrent/future.ML Wed Aug 10 16:24:39 2011 +0200
1.2 +++ b/src/Pure/Concurrent/future.ML Wed Aug 10 16:26:05 2011 +0200
1.3 @@ -39,6 +39,7 @@
1.4 val task_of: 'a future -> Task_Queue.task
1.5 val peek: 'a future -> 'a Exn.result option
1.6 val is_finished: 'a future -> bool
1.7 + val interruptible_task: ('a -> 'b) -> 'a -> 'b
1.8 val cancel_group: Task_Queue.group -> unit
1.9 val cancel: 'a future -> unit
1.10 type fork_params =
1.11 @@ -57,7 +58,6 @@
1.12 val promise: unit -> 'a future
1.13 val fulfill_result: 'a future -> 'a Exn.result -> unit
1.14 val fulfill: 'a future -> 'a -> unit
1.15 - val interruptible_task: ('a -> 'b) -> 'a -> 'b
1.16 val shutdown: unit -> unit
1.17 val status: (unit -> 'a) -> 'a
1.18 end;