--- a/src/Pure/Concurrent/future.ML Sun Jul 04 00:05:32 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Sun Jul 04 21:01:22 2010 +0200
@@ -59,6 +59,7 @@
val cancel_group: group -> unit
val cancel: 'a future -> unit
val shutdown: unit -> unit
+ val report: (unit -> 'a) -> 'a
end;
structure Future: FUTURE =
@@ -523,6 +524,16 @@
else ();
+(* report markup *)
+
+fun report e =
+ let
+ val _ = Output.status (Markup.markup Markup.forked "");
+ val x = e (); (*sic -- report "joined" only for success*)
+ val _ = Output.status (Markup.markup Markup.joined "");
+ in x end;
+
+
(*final declarations of this structure!*)
val map = map_future;