# HG changeset patch
# User wenzelm
# Date 1451997658 -3600
# Node ID 6dbeafce6318b2033d86a0ff16157e1fc069b274
# Parent  cff7114e45720a7fcf2f76ea91d248bcde9caeeb
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;

diff -r cff7114e4572 -r 6dbeafce6318 src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala	Tue Jan 05 13:40:58 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 =