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  

     2.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 04 00:05:32 2010 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jul 04 21:01:22 2010 +0200
     2.3 @@ -563,8 +563,8 @@
     2.4  
     2.5  fun async_state (tr as Transition {print, ...}) st =
     2.6    if print then
     2.7 -    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ())) (fn () =>
     2.8 -      setmp_thread_position tr (fn () => print_state false st) ()))
     2.9 +    ignore (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
    2.10 +      (fn () => Future.report (setmp_thread_position tr (fn () => print_state false st))))
    2.11    else ();
    2.12  
    2.13  fun error_msg tr exn_info =

     3.1 --- a/src/Pure/goal.ML	Sun Jul 04 00:05:32 2010 +0200
     3.2 +++ b/src/Pure/goal.ML	Sun Jul 04 21:01:22 2010 +0200
     3.3 @@ -104,12 +104,7 @@
     3.4  
     3.5  (* parallel proofs *)
     3.6  
     3.7 -fun fork e = Future.fork_pri ~1 (fn () =>
     3.8 -  let
     3.9 -    val _ = Output.status (Markup.markup Markup.forked "");
    3.10 -    val x = e ();  (*sic*)
    3.11 -    val _ = Output.status (Markup.markup Markup.joined "");
    3.12 -  in x end);
    3.13 +fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
    3.14  
    3.15  val parallel_proofs = Unsynchronized.ref 1;
    3.16