1.1 --- a/src/Pure/Concurrent/future.ML	Sun Jul 04 00:05:32 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sun Jul 04 21:01:22 2010 +0200
     1.3 @@ -59,6 +59,7 @@
     1.4    val cancel_group: group -> unit
     1.5    val cancel: 'a future -> unit
     1.6    val shutdown: unit -> unit
     1.7 +  val report: (unit -> 'a) -> 'a
     1.8  end;
     1.9  
    1.10  structure Future: FUTURE =
    1.11 @@ -523,6 +524,16 @@
    1.12    else ();
    1.13  
    1.14  
    1.15 +(* report markup *)
    1.16 +
    1.17 +fun report e =
    1.18 +  let
    1.19 +    val _ = Output.status (Markup.markup Markup.forked "");
    1.20 +    val x = e ();  (*sic -- report "joined" only for success*)
    1.21 +    val _ = Output.status (Markup.markup Markup.joined "");
    1.22 +  in x end;
    1.23 +
    1.24 +
    1.25  (*final declarations of this structure!*)
    1.26  val map = map_future;
    1.27