diff -r 25d6f789618b -r d8c7be27e01d src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Sun Aug 08 14:22:54 2010 +0200 +++ b/src/Pure/Concurrent/future.ML Sun Aug 08 19:36:31 2010 +0200 @@ -61,7 +61,7 @@ val cancel_group: group -> unit val cancel: 'a future -> unit val shutdown: unit -> unit - val report: (unit -> 'a) -> 'a + val status: (unit -> 'a) -> 'a end; structure Future: FUTURE = @@ -532,9 +532,9 @@ else (); -(* report markup *) +(* status markup *) -fun report e = +fun status e = let val _ = Output.status (Markup.markup Markup.forked ""); val x = e (); (*sic -- report "joined" only for success*)