--- a/src/Pure/Concurrent/future.ML Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Mar 18 16:26:35 2016 +0100
@@ -99,6 +99,13 @@
fun peek x = Single_Assignment.peek (result_of x);
fun is_finished x = is_some (peek x);
+val _ =
+ PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case peek x of
+ NONE => PolyML.PrettyString "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Res y) => pretty (y, depth)));
+
(** scheduling **)
@@ -665,4 +672,3 @@
end;
type 'a future = 'a Future.future;
-