# HG changeset patch
# User wenzelm
# Date 1586020699 -7200
# Node ID d5773922358d07ebc20d0d24462e9cf7d039e4a1
# Parent  5036edb025b75640938a262753e14dba17733821
clarified signature;

diff -r 5036edb025b7 -r d5773922358d src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -47,7 +47,7 @@
   private var active = true
   private val mailbox = Mailbox[Option[Request]]
 
-  private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
+  private val thread = Standard_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
   def is_active: Boolean = active && thread.isAlive
   def check_thread: Boolean = Thread.currentThread == thread
 
diff -r 5036edb025b7 -r d5773922358d src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/Concurrent/future.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -135,7 +135,7 @@
 {
   private val result = Future.promise[A]
   private val thread =
-    Standard_Thread.fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+    Standard_Thread.fork(name = name, daemon = daemon) { result.fulfill_result(Exn.capture(body)) }
 
   def peek: Option[Exn.Result[A]] = result.peek
   def join_result: Exn.Result[A] = result.join_result
diff -r 5036edb025b7 -r d5773922358d src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/Concurrent/standard_thread.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -21,10 +21,17 @@
 
   def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
 
-  def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Standard_Thread =
+  def fork(
+    name: String = "",
+    group: ThreadGroup = current_thread_group,
+    pri: Int = Thread.NORM_PRIORITY,
+    daemon: Boolean = false,
+    inherit_locals: Boolean = false)(body: => Unit): Standard_Thread =
   {
     val main = new Runnable { override def run { body } }
-    val thread = new Standard_Thread(current_thread_group, main, make_name(name = name), daemon)
+    val thread =
+      new Standard_Thread(main, name = make_name(name = name), group = group,
+        pri = pri, daemon = daemon, inherit_locals = inherit_locals)
     thread.start
     thread
   }
@@ -32,19 +39,13 @@
 
   /* self */
 
-  def self: Option[Standard_Thread] =
+  def self: Standard_Thread =
     Thread.currentThread match {
-      case thread: Standard_Thread => Some(thread)
-      case _ => None
+      case thread: Standard_Thread => thread
+      case _ => error("Expected to run on Isabelle/Scala standard thread")
     }
 
-  def uninterruptible[A](body: => A): A =
-  {
-    self match {
-      case Some(thread) => thread.uninterruptible(body)
-      case None => error("Cannot change interrupts --- running on non-standard thread")
-    }
-  }
+  def uninterruptible[A](body: => A): A = self.uninterruptible(body)
 
 
   /* pool */
@@ -56,7 +57,7 @@
       val executor =
         new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
       executor.setThreadFactory(
-        new Standard_Thread(current_thread_group, _, make_name(base = "worker"), false))
+        new Standard_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
       executor
     }
 
@@ -120,11 +121,18 @@
     new Delay(false, delay, log, event)
 }
 
-class Standard_Thread private(group: ThreadGroup, main: Runnable, name: String, daemon: Boolean)
-  extends Thread(group, null, name)
+class Standard_Thread private(
+    main: Runnable,
+    name: String = "",
+    group: ThreadGroup = null,
+    pri: Int = Thread.NORM_PRIORITY,
+    daemon: Boolean = false,
+    inherit_locals: Boolean = false)
+  extends Thread(group, null, name, 0L, inherit_locals)
 {
   thread =>
 
+  thread.setPriority(pri)
   thread.setDaemon(daemon)
 
   override def run { main.run() }
diff -r 5036edb025b7 -r d5773922358d src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/General/file_watcher.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -90,7 +90,7 @@
       handle(changed)
     }
 
-    private val watcher_thread = Standard_Thread.fork("File_Watcher", daemon = true)
+    private val watcher_thread = Standard_Thread.fork(name = "File_Watcher", daemon = true)
     {
       try {
         while (true) {
diff -r 5036edb025b7 -r d5773922358d src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/PIDE/prover.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -112,7 +112,7 @@
     }
   }
 
-  private val process_manager = Standard_Thread.fork("process_manager")
+  private val process_manager = Standard_Thread.fork(name = "process_manager")
   {
     val stdout = physical_output(false)
 
@@ -218,7 +218,7 @@
       if (err) ("standard_error", process.stderr, Markup.STDERR)
       else ("standard_output", process.stdout, Markup.STDOUT)
 
-    Standard_Thread.fork(name) {
+    Standard_Thread.fork(name = name) {
       try {
         var result = new StringBuilder(100)
         var finished = false
@@ -256,7 +256,7 @@
     class Protocol_Error(msg: String) extends Exception(msg)
 
     val name = "message_output"
-    Standard_Thread.fork(name) {
+    Standard_Thread.fork(name = name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
diff -r 5036edb025b7 -r d5773922358d src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Pure/Tools/server.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -292,7 +292,7 @@
     val progress: Connection_Progress = context.progress(ident)
     def cancel { progress.stop }
 
-    private lazy val thread = Standard_Thread.fork("server_task")
+    private lazy val thread = Standard_Thread.fork(name = "server_task")
     {
       Exn.capture { body(task) } match {
         case Exn.Res(res) =>
@@ -601,12 +601,12 @@
   }
 
   private lazy val server_thread: Thread =
-    Standard_Thread.fork("server") {
+    Standard_Thread.fork(name = "server") {
       var finished = false
       while (!finished) {
         Exn.capture(server_socket.accept) match {
           case Exn.Res(socket) =>
-            Standard_Thread.fork("server_connection")
+            Standard_Thread.fork(name = "server_connection")
               { using(Server.Connection(socket))(handle) }
           case Exn.Exn(_) => finished = true
         }
diff -r 5036edb025b7 -r d5773922358d src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Tools/jEdit/src/active.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -31,14 +31,14 @@
             // FIXME avoid hard-wired stuff
             elem match {
               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
-                Standard_Thread.fork("browser") {
+                Standard_Thread.fork(name = "browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
                   Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
                 }
 
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
-                Standard_Thread.fork("graphview") {
+                Standard_Thread.fork(name = "graphview") {
                   val graph =
                     Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
diff -r 5036edb025b7 -r d5773922358d src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -181,7 +181,7 @@
     if (path.is_file)
       goto_file(true, view, File.platform_path(path))
     else {
-      Standard_Thread.fork("documentation") {
+      Standard_Thread.fork(name = "documentation") {
         try { Doc.view(path) }
         catch {
           case exn: Throwable =>
@@ -211,7 +211,7 @@
     new Hyperlink {
       override val external = true
       def follow(view: View): Unit =
-        Standard_Thread.fork("hyperlink_url") {
+        Standard_Thread.fork(name = "hyperlink_url") {
           try { Isabelle_System.open(Url.escape_name(name)) }
           catch {
             case exn: Throwable =>
diff -r 5036edb025b7 -r d5773922358d src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -154,7 +154,7 @@
         }
         if (required_files.nonEmpty) {
           try {
-            Standard_Thread.fork("resolve_dependencies") {
+            Standard_Thread.fork(name = "resolve_dependencies") {
               val loaded_files =
                 for {
                   name <- required_files
diff -r 5036edb025b7 -r d5773922358d src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Apr 04 18:13:05 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Apr 04 19:18:19 2020 +0200
@@ -165,7 +165,7 @@
     setLocationRelativeTo(view)
     setVisible(true)
 
-    Standard_Thread.fork("session_build") {
+    Standard_Thread.fork(name = "session_build") {
       progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
 
       val (out, rc) =