# HG changeset patch
# User wenzelm
# Date 1223580851 -7200
# Node ID 2a6297b4273c9953f1554b1f082090d9a9c106de
# Parent  6a661aeff5643d2bfd47eda384606e34aa2e3ada
replaced str_of by general peek;

diff -r 6a661aeff564 -r 2a6297b4273c src/Pure/Concurrent/future.ML
--- 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);