# HG changeset patch
# User wenzelm
# Date 1601386247 -7200
# Node ID 41a4352c52400405caa3fe5412dec68ef18117c8
# Parent  b8708212bdd5ad9dbffd7372bc00c16d41c47317
more robust executor policy after shutdown;

diff -r b8708212bdd5 -r 41a4352c5240 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Tue Sep 29 15:05:37 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Tue Sep 29 15:30:47 2020 +0200
@@ -8,7 +8,7 @@
 
 import isabelle._
 
-import java.util.concurrent.Executors
+import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor}
 
 import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
 import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
@@ -46,8 +46,10 @@
     /* executor */
 
     val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads
+    val executor: ThreadPoolExecutor =
+      new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS,
+        new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy)
 
-    val executor = Executors.newFixedThreadPool(pool_size)
     val executor_killed = Synchronized(false)
     def executor_kill(): Unit =
       executor_killed.change(b =>