--- 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
--- 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
--- 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() }
--- 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) {
--- 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
--- 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
}
--- 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) }
--- 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 =>
--- 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
--- 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) =