# HG changeset patch
# User wenzelm
# Date 1222089974 -7200
# Node ID c6aef67f964d5469549f7319b38067c40161ea0f
# Parent  13cb2108c2b9f81f326ad97689d52be7d580b4c8
added is_finished;

diff -r 13cb2108c2b9 -r c6aef67f964d src/Pure/Concurrent/future.ML
--- 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 **)