equal
deleted
inserted
replaced
550 |
550 |
551 (* status markup *) |
551 (* status markup *) |
552 |
552 |
553 fun status e = |
553 fun status e = |
554 let |
554 let |
555 val _ = Output.status (Markup.markup Markup.forked ""); |
555 val task_props = |
|
556 (case worker_task () of |
|
557 NONE => I |
|
558 | SOME task => Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]); |
|
559 val _ = Output.status (Markup.markup (task_props Markup.forked) ""); |
556 val x = e (); (*sic -- report "joined" only for success*) |
560 val x = e (); (*sic -- report "joined" only for success*) |
557 val _ = Output.status (Markup.markup Markup.joined ""); |
561 val _ = Output.status (Markup.markup (task_props Markup.joined) ""); |
558 in x end; |
562 in x end; |
559 |
563 |
560 |
564 |
561 (*final declarations of this structure!*) |
565 (*final declarations of this structure!*) |
562 val map = map_future; |
566 val map = map_future; |