--- a/src/Pure/Concurrent/isabelle_thread.scala Sat Feb 24 10:21:41 2024 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Sat Feb 24 10:55:16 2024 +0100
@@ -65,7 +65,7 @@
val thread =
create(main, name = name, group = group, pri = pri,
daemon = daemon, inherit_locals = inherit_locals)
- thread.start
+ thread.start()
thread
}
@@ -89,10 +89,10 @@
new Interrupt_Handler(handle, name)
val interruptible: Interrupt_Handler =
- Interrupt_Handler(_.raise_interrupt, name = "interruptible")
+ Interrupt_Handler(_.raise_interrupt(), name = "interruptible")
val uninterruptible: Interrupt_Handler =
- Interrupt_Handler(_.postpone_interrupt, name = "uninterruptible")
+ Interrupt_Handler(_.postpone_interrupt(), name = "uninterruptible")
}
class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String)
@@ -132,7 +132,7 @@
thread.setPriority(pri)
thread.setDaemon(daemon)
- override def run: Unit = main.run()
+ override def run(): Unit = main.run()
def is_self: Boolean = Thread.currentThread == thread
@@ -142,19 +142,19 @@
// synchronized, with concurrent changes
private var interrupt_postponed: Boolean = false
- def clear_interrupt: Boolean = synchronized {
+ def clear_interrupt(): Boolean = synchronized {
val was_interrupted = isInterrupted || interrupt_postponed
Exn.Interrupt.dispose()
interrupt_postponed = false
was_interrupted
}
- def raise_interrupt: Unit = synchronized {
+ def raise_interrupt(): Unit = synchronized {
interrupt_postponed = false
super.interrupt()
}
- def postpone_interrupt: Unit = synchronized {
+ def postpone_interrupt(): Unit = synchronized {
interrupt_postponed = true
Exn.Interrupt.dispose()
}
@@ -175,12 +175,12 @@
val old_handler = handler
handler = new_handler
try {
- if (clear_interrupt) interrupt()
+ if (clear_interrupt()) interrupt()
body
}
finally {
handler = old_handler
- if (clear_interrupt) interrupt()
+ if (clear_interrupt()) interrupt()
}
}
}