# HG changeset patch
# User wenzelm
# Date 1222716406 -7200
# Node ID bf08f955e7dbbfd5017d55efca2c85f5f714bd6d
# Parent  419954d268863098a9b20ab86ecc15df19f2b344
added str_of;

diff -r 419954d26886 -r bf08f955e7db src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Sep 29 21:26:44 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 29 21:26:46 2008 +0200
@@ -33,6 +33,7 @@
   type 'a T
   val task_of: 'a T -> task
   val group_of: 'a T -> group
+  val str_of: 'a T -> string
   val is_finished: 'a T -> bool
   val future: group option -> task list -> bool -> (unit -> 'a) -> 'a T
   val fork: (unit -> 'a) -> 'a T
@@ -72,6 +73,12 @@
 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);