src/Pure/Concurrent/isabelle_thread.scala

       if (uninterruptible) { () => Isabelle_Thread.uninterruptible { body } }
       else { () => body }
     val thread =
       create(main, name = name, group = group, pri = pri,
         daemon = daemon, inherit_locals = inherit_locals)
-    thread.start
+    thread.start()
     thread
   }
 
 
   /* thread pool */

   object Interrupt_Handler {
     def apply(handle: Isabelle_Thread => Unit, name: String = "handler"): Interrupt_Handler =
       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)
     extends Function[Isabelle_Thread, Unit] {
     def apply(thread: Isabelle_Thread): Unit = handle(thread)

   thread =>
 
   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
 
 
   /* interrupt state */
 
   // 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()
   }
 
 

       require(is_self, "interrupt handler on other thread")
 
       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()
       }
     }
 }