replaced str_of by general peek;
authorwenzelm
Thu, 09 Oct 2008 21:34:11 +0200
changeset 28558 2a6297b4273c
parent 28557 6a661aeff564
child 28559 55c003a5600a
replaced str_of by general peek;
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);