# HG changeset patch
# User wenzelm
# Date 1586169360 -7200
# Node ID 8ec5c82b67dcf80cf7130b2080492b13713431fc
# Parent  0098b1974393df92f9daacbfa097660b73b0b4ed
tuned;

diff -r 0098b1974393 -r 8ec5c82b67dc src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 12:28:44 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Mon Apr 06 12:36:00 2020 +0200
@@ -12,7 +12,16 @@
 
 object Isabelle_Thread
 {
-  /* fork */
+  /* self-thread */
+
+  def self: Isabelle_Thread =
+    Thread.currentThread match {
+      case thread: Isabelle_Thread => thread
+      case _ => error("Isabelle-specific thread required")
+    }
+
+
+  /* fork threads */
 
   private val counter = Counter.make()
 
@@ -40,13 +49,18 @@
   }
 
 
-  /* self-thread */
+  /* thread pool */
 
-  def self: Isabelle_Thread =
-    Thread.currentThread match {
-      case thread: Isabelle_Thread => thread
-      case _ => error("Isabelle-specific thread required")
-    }
+  lazy val pool: ThreadPoolExecutor =
+  {
+    val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+    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(
+      new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
+    executor
+  }
 
 
   /* interrupt handlers */
@@ -83,20 +97,6 @@
     interrupt_handler(Interrupt_Handler.uninterruptible)(body)
 
 
-  /* thread pool */
-
-  lazy val pool: ThreadPoolExecutor =
-    {
-      val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
-      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(
-        new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
-      executor
-    }
-
-
   /* delayed events */
 
   final class Delay private[Isabelle_Thread](