diff -r 2375b38a42f8 -r d2dc9bc3a3e1 src/Pure/Concurrent/isabelle_thread.scala --- a/src/Pure/Concurrent/isabelle_thread.scala Thu Aug 13 13:18:17 2020 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.scala Thu Aug 13 14:41:28 2020 +0200 @@ -33,6 +33,9 @@ def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup + lazy val worker_thread_group: ThreadGroup = + new ThreadGroup(current_thread_group, "Isabelle worker") + def create( main: Runnable, name: String = "", @@ -72,7 +75,8 @@ val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 val executor = new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) - executor.setThreadFactory(create(_, name = make_name(base = "worker"), group = current_thread_group)) + executor.setThreadFactory( + create(_, name = make_name(base = "worker"), group = worker_thread_group)) executor }