--- a/src/Pure/Concurrent/future.ML Thu Oct 09 21:34:05 2008 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Oct 09 21:34:11 2008 +0200
@@ -33,7 +33,7 @@
type 'a T
val task_of: 'a T -> task
val group_of: 'a T -> group
- val str_of: 'a T -> string
+ val peek: 'a T -> 'a Exn.result option
val is_finished: 'a T -> bool
val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
val fork: (unit -> 'a) -> 'a T
@@ -72,13 +72,8 @@
fun task_of (Future {task, ...}) = task;
fun group_of (Future {group, ...}) = group;
-fun str_of (Future {result, ...}) =
- (case ! result of
- NONE => "<future>"
- | SOME (Exn.Result _) => "<finished future>"
- | SOME (Exn.Exn _) => "<failed future>");
-
-fun is_finished (Future {result, ...}) = is_some (! result);
+fun peek (Future {result, ...}) = ! result;
+fun is_finished x = is_some (peek x);