--- a/src/Pure/Concurrent/future.ML Mon Sep 22 15:26:13 2008 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Sep 22 15:26:14 2008 +0200
@@ -32,6 +32,7 @@
type 'a T
val task_of: 'a T -> task
val group_of: 'a T -> group
+ val is_finished: 'a T -> bool
val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
val fork: (unit -> 'a) -> 'a T
val fork_irrelevant: (unit -> 'a) -> 'a T
@@ -69,6 +70,8 @@
fun task_of (Future {task, ...}) = task;
fun group_of (Future {group, ...}) = group;
+fun is_finished (Future {result, ...}) = is_some (! result);
+
(** scheduling **)