# HG changeset patch
# User wenzelm
# Date 1596636997 -7200
# Node ID 41e1e2395a67e9ab01a23d428d91fc02dc2481a6
# Parent  3afd6b1c7ab5aba8f744ebef52c7bf5376faba54
avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;

diff -r 3afd6b1c7ab5 -r 41e1e2395a67 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Aug 05 12:42:43 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 05 16:16:37 2020 +0200
@@ -320,11 +320,14 @@
     val max_active0 = ! max_active;
     val max_workers0 = ! max_workers;
 
+    val workers_waiting = count_workers Waiting;
+
     val m =
       if ! do_shutdown andalso Task_Queue.all_passive (! queue) then 0
       else Multithreading.max_threads ();
     val _ = max_active := m;
-    val _ = max_workers := 2 * m;
+    val _ = max_workers :=
+      Int.max (2 * m, if workers_waiting > 0 then workers_waiting + 1 else 0);
 
     val missing = ! max_workers - length (! workers);
     val _ =