# HG changeset patch
# User wenzelm
# Date 1313188494 -7200
# Node ID aaaa13e297dc33d017a195b9349624fb3861e228
# Parent  21f97048b478eadc4dec59bef97785648c0aa03c
immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
more careful treatment of last_round on startup/shutdown;

diff -r 21f97048b478 -r aaaa13e297dc src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Aug 12 23:29:28 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Aug 13 00:34:54 2011 +0200
@@ -310,7 +310,7 @@
     val _ =
       if mm = 0 orelse ! worker_trend > 50 orelse ! worker_trend < ~50 then
         max_workers := mm
-      else if ! worker_trend > 5 andalso ! max_workers < 2 * m then
+      else if ! worker_trend > 5 andalso ! max_workers < 2 * m orelse ! max_workers = 0 then
         max_workers := Int.min (mm, 2 * m)
       else ();
 
@@ -358,11 +358,11 @@
     else reraise exn;
 
 fun scheduler_loop () =
-  while
+ (while
     Multithreading.with_attributes
       (Multithreading.sync_interrupts Multithreading.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
-  do ();
+  do (); last_round := Time.zeroTime);
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);