# 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!*)