# HG changeset patch
# User wenzelm
# Date 1596025399 -7200
# Node ID b8d0b8659e0a0b436ae525e96c7a0f721d039c1e
# Parent  1d6c3cba47fec706634ec5a5b7e7cb5266942d91
more robust scheduler shutdown, notably for spurious crashes;

diff -r 1d6c3cba47fe -r b8d0b8659e0a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Jul 27 15:58:43 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Jul 29 14:23:19 2020 +0200
@@ -285,6 +285,9 @@
 
 (* scheduler *)
 
+fun scheduler_end () = (*requires SYNCHRONIZED*)
+  (report_status (); scheduler := NONE);
+
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     val now = Time.now ();
@@ -354,16 +357,18 @@
     (* shutdown *)
 
     val continue = not (! do_shutdown andalso null (! workers));
-    val _ = if continue then () else (report_status (); scheduler := NONE);
+    val _ = if continue then () else scheduler_end ();
 
     val _ = broadcast scheduler_event;
   in continue end
   handle exn =>
+   (Multithreading.tracing 1 (fn () => "SCHEDULER: " ^ General.exnMessage exn);
     if Exn.is_interrupt exn then
-     (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
-      List.app cancel_later (cancel_all ());
+     (List.app cancel_later (cancel_all ());
       signal work_available; true)
-    else Exn.reraise exn;
+    else
+     (scheduler_end ();
+      Exn.reraise exn));
 
 fun scheduler_loop () =
  (while
@@ -705,7 +710,7 @@
       while scheduler_active () do
        (do_shutdown := true;
         Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
-        wait scheduler_event));
+        wait_timeout next_round scheduler_event));
 
 
 (*final declarations of this structure!*)