discontinued worker_trend: prefer constant number of active + reserve threads;
tuned exceptional situations;

--- a/src/Pure/Concurrent/future.ML	Sat Jan 10 11:48:52 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Jan 10 12:21:27 2015 +0100
@@ -140,7 +140,6 @@
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
 val max_active = Unsynchronized.ref 0;
-val worker_trend = Unsynchronized.ref 0;
 
 val status_ticks = Unsynchronized.ref 0;
 val last_round = Unsynchronized.ref Time.zeroTime;
@@ -265,7 +264,7 @@
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
     Unsynchronized.ref Working))
-  handle Fail msg => Multithreading.tracing 0 (fn () => msg);
+  handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
 
 
 
@@ -287,7 +286,7 @@
       then report_status () else ();
 
     val _ =
-      if forall (Thread.isActive o #1) (! workers) then ()
+      if not tick orelse forall (Thread.isActive o #1) (! workers) then ()
       else
         let
           val (alive, dead) = List.partition (Thread.isActive o #1) (! workers);
@@ -305,22 +304,7 @@
 
     val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
     val _ = max_active := m;
-
-    val mm =
-      if ! do_shutdown then 0
-      else Int.min (Int.max (count_workers Working + 2 * count_workers Waiting, m), 4 * m);
-    val _ =
-      if tick andalso mm > ! max_workers then
-        Unsynchronized.change worker_trend (fn w => if w < 0 then 0 else w + 1)
-      else if tick andalso mm < ! max_workers then
-        Unsynchronized.change worker_trend (fn w => if w > 0 then 0 else w - 1)
-      else ();
-    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 orelse ! max_workers = 0 then
-        max_workers := Int.min (mm, 2 * m)
-      else ();
+    val _ = max_workers := 2 * m;
 
     val missing = ! max_workers - length (! workers);
     val _ =