src/Pure/Concurrent/future.ML
changeset 50683 34b109c5324c
parent 50664 fff984a77f58
child 50909 b2fb1ab1475d
equal deleted inserted replaced
50682:a0888c03a727 50683:34b109c5324c
   202         ("workers_total", Markup.print_int total),
   202         ("workers_total", Markup.print_int total),
   203         ("workers_active", Markup.print_int active),
   203         ("workers_active", Markup.print_int active),
   204         ("workers_waiting", Markup.print_int waiting)] @
   204         ("workers_waiting", Markup.print_int waiting)] @
   205         ML_Statistics.get ();
   205         ML_Statistics.get ();
   206     in
   206     in
   207       Output.protocol_message (Markup.ML_statistics @ stats) ""
   207       Output.protocol_message (Markup.ML_statistics :: stats) ""
   208         handle Fail msg => warning msg
   208         handle Fail msg => warning msg
   209     end
   209     end
   210   else ();
   210   else ();
   211 
   211 
   212 
   212