equal
deleted
inserted
replaced
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 |