# HG changeset patch
# User wenzelm
# Date 1361882314 -3600
# Node ID fefd0769797918b582d623dd50922306a36bd627
# Parent  3d3c1ea0a4013041e7dc014096084168c0c99b74
disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;

diff -r 3d3c1ea0a401 -r fefd07697979 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Feb 26 13:27:24 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Tue Feb 26 13:38:34 2013 +0100
@@ -678,12 +678,14 @@
 (* shutdown *)
 
 fun shutdown () =
-  if Multithreading.available then
+  if not Multithreading.available then ()
+  else if is_some (worker_task ()) then
+    raise Fail "Cannot shutdown while running as worker thread"
+  else
     SYNCHRONIZED "shutdown" (fn () =>
       while scheduler_active () do
        (Multithreading.tracing 1 (fn () => "SHUTDOWN: wait");
-        wait scheduler_event))
-  else ();
+        wait scheduler_event));
 
 
 (*final declarations of this structure!*)