src/Pure/Concurrent/future.ML
changeset 60764 b610ba36e02c
parent 60610 f52b4b0c10c4
child 60911 858694df711b
--- 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));