merged

--- a/src/Pure/Concurrent/future.ML	Wed Aug 05 08:47:45 2020 +0000
+++ b/src/Pure/Concurrent/future.ML	Wed Aug 05 17:19:35 2020 +0200
@@ -27,7 +27,7 @@
   val default_params: params
   val forks: params -> (unit -> 'a) list -> 'a future list
   val fork: (unit -> 'a) -> 'a future
-  val get_finished: 'a future -> 'a
+  val get_result: 'a future -> 'a Exn.result
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val joins: 'a future list -> 'a list
@@ -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 _ =
@@ -508,8 +511,6 @@
         | exns => Exn.Exn (Par_Exn.make exns))
       else res);
 
-fun get_finished x = Exn.release (get_result x);
-
 local
 
 fun join_next atts deps = (*requires SYNCHRONIZED*)

--- a/src/Pure/Concurrent/lazy.ML	Wed Aug 05 08:47:45 2020 +0000
+++ b/src/Pure/Concurrent/lazy.ML	Wed Aug 05 17:19:35 2020 +0200
@@ -103,7 +103,7 @@
                   let
                     val res0 = Exn.capture (restore_attributes e) ();
                     val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                    val res = Future.join_result x;
+                    val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
                         Synchronized.assign var (Result (Future.value_result res))