disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;
--- 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!*)