# HG changeset patch
# User wenzelm
# Date 1420896521 -3600
# Node ID 734bb148503e2993eff994ad9a3c80d306134b64
# Parent  abc53a03ca1c56c3c739831f8b85215e7c137deb
explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image;
discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;

diff -r abc53a03ca1c -r 734bb148503e src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Jan 10 13:02:27 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Sat Jan 10 14:28:41 2015 +0100
@@ -302,7 +302,9 @@
     val max_active0 = ! max_active;
     val max_workers0 = ! max_workers;
 
-    val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
+    val m =
+      if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
+      else Multithreading.max_threads_value ();
     val _ = max_active := m;
     val _ = max_workers := 2 * m;
 
@@ -336,7 +338,6 @@
 
     (* shutdown *)
 
-    val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else ();
     val continue = not (! do_shutdown andalso null (! workers));
     val _ = if continue then () else (report_status (); scheduler := NONE);
 
@@ -657,7 +658,8 @@
   else
     SYNCHRONIZED "shutdown" (fn () =>
       while scheduler_active () do
-       (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
+       (do_shutdown := true;
+        Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
         wait scheduler_event));