# HG changeset patch # User wenzelm # Date 1248989873 -7200 # Node ID e0b8da3fae4db4ec86053aa4ba3f7ef7696f87a3 # Parent ceb7190d7a5260551a91d1bc92885ec4674e0e19 tuned tracing; diff -r ceb7190d7a52 -r e0b8da3fae4d src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Jul 30 23:23:52 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Jul 30 23:37:53 2009 +0200 @@ -269,7 +269,11 @@ (*canceled groups*) val _ = if null (! canceled) then () - else (change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_work ()); + else + (Multithreading.tracing 1 (fn () => + string_of_int (length (! canceled)) ^ " canceled groups"); + change canceled (filter_out (Task_Queue.cancel (! queue))); + broadcast_work ()); (*delay loop*) val _ = wait_interruptible next_round scheduler_event