# HG changeset patch
# User wenzelm
# Date 1708768516 -3600
# Node ID f33d37c171a9f41013da0d3536b7bd255a473939
# Parent  e59d93da9109a84797df84be5d446918859ba2cc
clarified signature: fewer warnings in IntelliJ IDEA;

diff -r e59d93da9109 -r f33d37c171a9 src/Pure/Concurrent/isabelle_thread.scala
--- 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()
       }
     }
 }