# HG changeset patch
# User wenzelm
# Date 1451997689 -3600
# Node ID af58628952f0589e85330ddaf5a82e36d54debd8
# Parent  755fda743c49415efc12e963ea0af1a05102206a# Parent  6dbeafce6318b2033d86a0ff16157e1fc069b274
merged

diff -r 755fda743c49 -r af58628952f0 src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Tue Jan 05 13:35:06 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala	Tue Jan 05 13:41:29 2016 +0100
@@ -9,7 +9,7 @@
 
 
 import java.lang.Thread
-import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue}
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
 
 import scala.concurrent.{ExecutionContext, ExecutionContextExecutor}
 
@@ -35,7 +35,19 @@
     {
       val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
       val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
-      new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+      val executor =
+        new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+      val old_thread_factory = executor.getThreadFactory
+      executor.setThreadFactory(
+        new ThreadFactory {
+          def newThread(r: Runnable) =
+          {
+            val thread = old_thread_factory.newThread(r)
+            thread.setDaemon(true)
+            thread
+          }
+        })
+      executor
     }
 
   lazy val execution_context: ExecutionContextExecutor =