report status more frequently on demand;
authorwenzelm
Thu, 24 Jan 2013 17:31:12 +0100
changeset 5201426a0984191b3
parent 52013 630c0895d9d1
child 52015 2ad5c46bcd04
report status more frequently on demand;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Thu Jan 24 17:18:13 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Thu Jan 24 17:31:12 2013 +0100
     1.3 @@ -318,9 +318,10 @@
     1.4      (* runtime status *)
     1.5  
     1.6      val _ =
     1.7 -      if tick then Unsynchronized.change status_ticks (fn i => (i + 1) mod 10) else ();
     1.8 +      if tick then Unsynchronized.change status_ticks (fn i => i + 1) else ();
     1.9      val _ =
    1.10 -      if tick andalso ! status_ticks = 0 then report_status () else ();
    1.11 +      if tick andalso ! status_ticks mod (if ! Multithreading.trace >= 1 then 2 else 10) = 0
    1.12 +      then report_status () else ();
    1.13  
    1.14      val _ =
    1.15        if forall (Thread.isActive o #1) (! workers) then ()