--- a/src/Pure/Concurrent/future.ML Tue Jul 21 14:07:06 2015 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Jul 21 14:12:45 2015 +0200
@@ -264,7 +264,7 @@
Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
val worker =
- Simple_Thread.fork {stack_limit = stack_limit, interrupts = false}
+ Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
(fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -366,7 +366,9 @@
(do_shutdown := false;
if scheduler_active () then ()
else
- scheduler := SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} scheduler_loop));
+ scheduler :=
+ SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+ scheduler_loop));