# HG changeset patch
# User wenzelm
# Date 1222984332 -7200
# Node ID 409fedeece30aa88e4bcaf4fc7d32c4ba6fa5c15
# Parent  0946c81ab77b62e28c1d99fc7f71147dce47049e
added simple heartbeat thread;

diff -r 0946c81ab77b -r 409fedeece30 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Oct 02 23:52:10 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 02 23:52:12 2008 +0200
@@ -188,6 +188,11 @@
 
 (* scheduler *)
 
+fun heartbeat name =
+ (Multithreading.tracing 1 (fn () => name);
+  OS.Process.sleep (Time.fromMilliseconds 100);
+  if ! do_shutdown then () else heartbeat name);
+
 fun scheduler_next () = (*requires SYNCHRONIZED*)
   let
     (*worker threads*)
@@ -227,7 +232,8 @@
 fun scheduler_check name = SYNCHRONIZED name (fn () =>
   if not (scheduler_active ()) then
     (Multithreading.tracing 2 (fn () => "scheduler: fork");
-     do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
+     do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop);
+     SimpleThread.fork false (fn () => heartbeat ("heartbeat " ^ string_of_int (inc next))); ())
   else if ! do_shutdown then error "Scheduler shutdown in progress"
   else ());
 
@@ -321,7 +327,8 @@
       do_shutdown := true;
       notify_all ();
       while not (null (! workers)) do wait "shutdown: workers";
-      while scheduler_active () do wait "shutdown: scheduler still active")))
+      while scheduler_active () do wait "shutdown: scheduler still active";
+      OS.Process.sleep (Time.fromMilliseconds 300))))
   else ();
 
 end;