clarified signature --- fewer warnings;
authorwenzelm
Thu, 04 Mar 2021 21:04:27 +0100
changeset 73614 77ef8bef0593
parent 73613 5f388e514ab8
child 73615 894f29abe5fc
clarified signature --- fewer warnings;
src/HOL/Tools/Nitpick/kodkod.scala
src/Pure/Concurrent/delay.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/isabelle_thread.scala
src/Pure/Concurrent/par_list.scala
src/Pure/GUI/gui.scala
src/Pure/General/exn.scala
src/Pure/General/file.scala
src/Pure/General/file_watcher.scala
src/Pure/General/http.scala
src/Pure/General/mailman.scala
src/Pure/General/scan.scala
src/Pure/General/sql.scala
src/Pure/General/ssh.scala
src/Pure/General/url.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_statistics.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/session.scala
src/Pure/System/bash.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/System/posix_interrupt.scala
src/Pure/System/progress.scala
src/Pure/System/scala.scala
src/Pure/System/system_channel.scala
src/Pure/System/tty_loop.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_job.scala
src/Pure/Tools/server.scala
src/Pure/Tools/spell_checker.scala
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/mutator_dialog.scala
src/Tools/VSCode/src/language_server.scala
src/Tools/jEdit/src-base/jedit_lib.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/jedit_spell_checker.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/process_indicator.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/session_build.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/text_overview.scala
src/Tools/jEdit/src/text_structure.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -96,7 +96,7 @@
     /* main */
 
     try {
-      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
+      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream()))
       val parser =
         KodkodiParser.create(context, executor,
           false, solve_all, prove, max_solutions, cleanup_inst, lexer)
@@ -114,7 +114,7 @@
       try { parser.problems() }
       catch { case exn: RecognitionException => parser.reportError(exn) }
 
-      timeout_request.foreach(_.cancel)
+      timeout_request.foreach(_.cancel())
 
       if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
         context.error("Error: trailing tokens")
--- a/src/Pure/Concurrent/delay.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/delay.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -37,7 +37,7 @@
   {
     val new_run =
       running match {
-        case Some(request) => if (first) false else { request.cancel; true }
+        case Some(request) => if (first) false else { request.cancel(); true }
         case None => true
       }
     if (new_run)
@@ -47,7 +47,7 @@
   def revoke(): Unit = synchronized
   {
     running match {
-      case Some(request) => request.cancel; running = None
+      case Some(request) => request.cancel(); running = None
       case None =>
     }
   }
@@ -57,7 +57,7 @@
     running match {
       case Some(request) =>
         val alt_time = Time.now() + alt_delay
-        if (request.time < alt_time && request.cancel) {
+        if (request.time < alt_time && request.cancel()) {
           running = Some(Event_Timer.request(alt_time)(run))
         }
       case None =>
--- a/src/Pure/Concurrent/event_timer.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/event_timer.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -19,7 +19,7 @@
 
   final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask)
   {
-    def cancel: Boolean = task.cancel
+    def cancel(): Boolean = task.cancel()
   }
 
   def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
--- a/src/Pure/Concurrent/future.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/future.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -38,7 +38,7 @@
   def join_result: Exn.Result[A]
   def join: A = Exn.release(join_result)
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }
-  def cancel: Unit
+  def cancel(): Unit
 
   override def toString: String =
     peek match {
@@ -61,7 +61,7 @@
 {
   val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
   def join_result: Exn.Result[A] = peek.get
-  def cancel: Unit = {}
+  def cancel(): Unit = {}
 }
 
 
@@ -93,7 +93,7 @@
     if (do_run) {
       val result = Exn.capture(body)
       status.change(_ => Terminated)
-      status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
+      status.change(_ => Finished(if (Thread.interrupted()) Exn.Exn(Exn.Interrupt()) else result))
     }
   }
   private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
@@ -107,11 +107,11 @@
     }
   }
 
-  def cancel =
+  def cancel(): Unit =
   {
     status.change {
       case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
-      case st @ Running(thread) => thread.interrupt; st
+      case st @ Running(thread) => thread.interrupt(); st
       case st => st
     }
   }
@@ -133,7 +133,7 @@
 
   def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
 
-  def cancel: Unit =
+  def cancel(): Unit =
     state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
 }
 
@@ -157,5 +157,5 @@
 
   def peek: Option[Exn.Result[A]] = result.peek
   def join_result: Exn.Result[A] = result.join_result
-  def cancel: Unit = thread.interrupt
+  def cancel(): Unit = thread.interrupt()
 }
--- a/src/Pure/Concurrent/isabelle_thread.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -174,7 +174,7 @@
   // non-synchronized, only changed on self-thread
   @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible
 
-  override def interrupt: Unit = handler(thread)
+  override def interrupt(): Unit = handler(thread)
 
   def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
     if (new_handler == null) body
@@ -184,12 +184,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()
       }
     }
 }
--- a/src/Pure/Concurrent/par_list.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -19,7 +19,7 @@
         state.change { case (futures, canceled) =>
           if (!canceled) {
             for ((future, i) <- futures.iterator.zipWithIndex if i != self)
-              future.cancel
+              future.cancel()
           }
           (futures, true)
         }
--- a/src/Pure/GUI/gui.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -22,10 +22,10 @@
 
   def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.install()
 
-  def current_laf(): String = UIManager.getLookAndFeel.getClass.getName()
+  def current_laf: String = UIManager.getLookAndFeel.getClass.getName()
 
-  def is_macos_laf(): Boolean =
-    Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf()
+  def is_macos_laf: Boolean =
+    Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf
 
   class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service
   {
--- a/src/Pure/General/exn.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/exn.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -102,9 +102,9 @@
     def apply(): Throwable = new InterruptedException("Interrupt")
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
-    def dispose(): Unit = Thread.interrupted
-    def expose(): Unit = if (Thread.interrupted) throw apply()
-    def impose(): Unit = Thread.currentThread.interrupt
+    def dispose(): Unit = Thread.interrupted()
+    def expose(): Unit = if (Thread.interrupted()) throw apply()
+    def impose(): Unit = Thread.currentThread.interrupt()
 
     val return_code = 130
   }
--- a/src/Pure/General/file.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/file.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -199,7 +199,7 @@
     val output = new StringBuilder(100)
     var c = -1
     while ({ c = reader.read; c != -1 }) output += c.toChar
-    reader.close
+    reader.close()
     output.toString
   }
 
@@ -233,7 +233,7 @@
       progress(line.get)
       result += line.get
     }
-    reader.close
+    reader.close()
     result.toList
   }
 
--- a/src/Pure/General/file_watcher.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/file_watcher.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -72,14 +72,14 @@
         st.dirs.get(dir) match {
           case None => st
           case Some(key) =>
-            key.cancel
+            key.cancel()
             st.copy(dirs = st.dirs - dir)
         })
 
     override def purge(retain: Set[JFile]): Unit =
       state.change(st =>
         st.copy(dirs = st.dirs --
-          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
+          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel(); dir })))
 
 
     /* changed directory entries */
@@ -127,9 +127,9 @@
 
     override def shutdown(): Unit =
     {
-      watcher_thread.interrupt
+      watcher_thread.interrupt()
       watcher_thread.join
-      delay_changed.revoke
+      delay_changed.revoke()
     }
   }
 }
--- a/src/Pure/General/http.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -109,8 +109,8 @@
     def += (handler: Handler): Unit = http_server.createContext(handler.root, handler.handler)
     def -= (handler: Handler): Unit = http_server.removeContext(handler.root)
 
-    def start: Unit = http_server.start
-    def stop: Unit = http_server.stop(0)
+    def start(): Unit = http_server.start
+    def stop(): Unit = http_server.stop(0)
 
     def address: InetSocketAddress = http_server.getAddress
     def url: String = "http://" + address.getHostName + ":" + address.getPort
--- a/src/Pure/General/mailman.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/mailman.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -55,7 +55,7 @@
               Some(path)
             }
           }
-          finally { connection.getInputStream.close }
+          finally { connection.getInputStream.close() }
         })
     }
   }
--- a/src/Pure/General/scan.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/scan.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -479,7 +479,7 @@
       def pos: InputPosition = new OffsetPosition(source, offset)
       def atEnd: Boolean = !seq.isDefinedAt(offset)
       override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n)
-      def close: Unit = buffered_stream.close
+      def close(): Unit = buffered_stream.close()
     }
     new Paged_Reader(0)
   }
--- a/src/Pure/General/sql.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/sql.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -253,7 +253,7 @@
     def execute(): Boolean = rep.execute()
     def execute_query(): Result = new Result(this, rep.executeQuery())
 
-    def close(): Unit = rep.close
+    def close(): Unit = rep.close()
   }
 
 
@@ -322,7 +322,7 @@
 
     def connection: Connection
 
-    def close(): Unit = connection.close
+    def close(): Unit = connection.close()
 
     def transaction[A](body: => A): A =
     {
@@ -483,7 +483,7 @@
       val connection = DriverManager.getConnection(url, user, password)
       new Database(name, connection, port_forwarding)
     }
-    catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn }
+    catch { case exn: Throwable => port_forwarding.foreach(_.close()); throw exn }
   }
 
   class Database private[PostgreSQL](
@@ -509,6 +509,6 @@
       table.insert_cmd("INSERT",
         sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
-    override def close(): Unit = { super.close; port_forwarding.foreach(_.close) }
+    override def close(): Unit = { super.close(); port_forwarding.foreach(_.close()) }
   }
 }
--- a/src/Pure/General/ssh.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/ssh.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -141,15 +141,15 @@
 
         val fw =
           try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) }
-          catch { case exn: Throwable => proxy.close; throw exn }
+          catch { case exn: Throwable => proxy.close(); throw exn }
 
         try {
           connect_session(host = fw.local_host, port = fw.local_port,
             host_key_permissive = permissive,
             nominal_host = host, nominal_user = user, user = user,
-            on_close = () => { fw.close; proxy.close })
+            on_close = () => { fw.close(); proxy.close() })
         }
-        catch { case exn: Throwable => fw.close; proxy.close; throw exn }
+        catch { case exn: Throwable => fw.close(); proxy.close(); throw exn }
       }
     }
   }
@@ -259,7 +259,7 @@
       progress_stderr: String => Unit = (_: String) => (),
       strict: Boolean = true): Process_Result =
     {
-      stdin.close
+      stdin.close()
 
       def read_lines(stream: InputStream, progress: String => Unit): List[String] =
       {
@@ -293,7 +293,7 @@
 
       def terminate(): Unit =
       {
-        close
+        close()
         out_lines.join
         err_lines.join
         exit_status.join
@@ -303,7 +303,7 @@
         try { exit_status.join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
-      close
+      close()
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join)
--- a/src/Pure/General/url.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/General/url.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -43,7 +43,7 @@
     catch { case ERROR(_) => false }
 
   def is_readable(name: String): Boolean =
-    try { Url(name).openStream.close; true }
+    try { Url(name).openStream.close(); true }
     catch { case ERROR(_) => false }
 
 
--- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -189,8 +189,8 @@
 
     def flush(): Unit =
     {
-      if (content.nonEmpty) { ship(content.toList); content.clear }
-      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
+      if (content.nonEmpty) { ship(content.toList); content.clear() }
+      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear() }
     }
 
     for (tok <- toks) {
@@ -199,7 +199,7 @@
         tok.is_command &&
           (!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
       { flush(); content += tok }
-      else { content ++= ignored; ignored.clear; content += tok }
+      else { content ++= ignored; ignored.clear(); content += tok }
     }
     flush()
 
--- a/src/Pure/ML/ml_console.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/ML/ml_console.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -74,7 +74,7 @@
             else Some(Sessions.base_info(
               options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
 
-      POSIX_Interrupt.handler { process.interrupt } {
+      POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join
         val rc = process.join
         if (rc != 0) sys.exit(rc)
--- a/src/Pure/ML/ml_statistics.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -93,7 +93,7 @@
     override def exit(): Unit = synchronized
     {
       session = null
-      monitoring.cancel
+      monitoring.cancel()
     }
 
     private def consume(props: Properties.T): Unit = synchronized
--- a/src/Pure/PIDE/headless.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/PIDE/headless.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -337,7 +337,7 @@
                         domain = Some(domain), trim = changed.assignment)
 
                     if (nodes_status_delay >= Time.zero && nodes_status_changed) {
-                      delay_nodes_status.invoke
+                      delay_nodes_status.invoke()
                     }
 
                     val theory_progress =
@@ -357,8 +357,8 @@
 
               if (commit.isDefined && commit_cleanup_delay > Time.zero) {
                 if (use_theories_state.value.finished_result)
-                  delay_commit_clean.revoke
-                else delay_commit_clean.invoke
+                  delay_commit_clean.revoke()
+                else delay_commit_clean.invoke()
               }
             }
         }
@@ -368,7 +368,7 @@
         session.commands_changed += consumer
         check_state()
         use_theories_state.guarded_access(_.join_result)
-        check_progress.cancel
+        check_progress.cancel()
       }
       finally {
         session.commands_changed -= consumer
@@ -575,7 +575,7 @@
 
       progress.echo("Starting session " + session_base_info.session + " ...")
       Isabelle_Process(session, options, session_base_info.sessions_structure, store,
-        logic = session_base_info.session, modes = print_mode).await_startup
+        logic = session_base_info.session, modes = print_mode).await_startup()
 
       session
     }
--- a/src/Pure/PIDE/prover.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/PIDE/prover.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -106,7 +106,7 @@
 
   private def terminate_process(): Unit =
   {
-    try { process.terminate }
+    try { process.terminate() }
     catch {
       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
     }
@@ -184,7 +184,7 @@
 
   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
 
-  private def command_input_close(): Unit = command_input.foreach(_.shutdown)
+  private def command_input_close(): Unit = command_input.foreach(_.shutdown())
 
   private def command_input_init(raw_stream: OutputStream): Unit =
   {
@@ -204,7 +204,7 @@
                 }
                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
             },
-          finish = { case () => stream.close; system_output(name + " terminated") }
+          finish = { case () => stream.close(); system_output(name + " terminated") }
         )
       )
   }
@@ -233,10 +233,10 @@
           }
           if (result.nonEmpty) {
             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
-            result.clear
+            result.clear()
           }
           else {
-            reader.close
+            reader.close()
             finished = true
           }
           //}}}
@@ -333,7 +333,7 @@
         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
         case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
       }
-      stream.close
+      stream.close()
 
       system_output(name + " terminated")
     }
--- a/src/Pure/PIDE/session.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -624,7 +624,7 @@
             delay_prune.revoke()
             if (prover.defined) {
               global_state.change(_ => Document.State.init)
-              prover.get.terminate
+              prover.get.terminate()
             }
 
           case Get_State(promise) =>
--- a/src/Pure/System/bash.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/bash.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -108,7 +108,7 @@
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
       kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
-      proc.destroy
+      proc.destroy()
       do_cleanup()
     }
 
@@ -173,7 +173,7 @@
       watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
-      stdin.close
+      stdin.close()
 
       val out_lines =
         Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
@@ -195,7 +195,7 @@
         try { join }
         catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
 
-      watchdog_thread.foreach(_.cancel)
+      watchdog_thread.foreach(_.cancel())
 
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
--- a/src/Pure/System/isabelle_process.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -37,7 +37,7 @@
           modes = modes, cwd = cwd, env = env)
       }
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
-    process.stdin.close
+    process.stdin.close()
 
     new Isabelle_Process(session, channel, process)
   }
@@ -77,5 +77,5 @@
     result
   }
 
-  def terminate: Unit = process.terminate
+  def terminate(): Unit = process.terminate()
 }
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -421,7 +421,7 @@
     proc.command(command_line:_*)  // fragile on Windows
     if (cwd != null) proc.directory(cwd)
     if (env != null) {
-      proc.environment.clear
+      proc.environment.clear()
       for ((x, y) <- env) proc.environment.put(x, y)
     }
     proc.redirectErrorStream(redirect)
@@ -430,15 +430,15 @@
 
   def process_output(proc: Process): (String, Int) =
   {
-    proc.getOutputStream.close
+    proc.getOutputStream.close()
 
     val output = File.read_stream(proc.getInputStream)
     val rc =
       try { proc.waitFor }
       finally {
-        proc.getInputStream.close
-        proc.getErrorStream.close
-        proc.destroy
+        proc.getInputStream.close()
+        proc.getErrorStream.close()
+        proc.destroy()
         Exn.Interrupt.dispose()
       }
     (output, rc)
--- a/src/Pure/System/isabelle_tool.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -157,7 +157,7 @@
 
   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
 
-Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
+Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage()
         case tool_name :: tool_args =>
           find_external(tool_name) orElse find_internal(tool_name) match {
             case Some(tool) => tool(tool_args)
--- a/src/Pure/System/posix_interrupt.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/posix_interrupt.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -23,7 +23,7 @@
   def exception[A](e: => A): A =
   {
     val thread = Thread.currentThread
-    handler { thread.interrupt } { e }
+    handler { thread.interrupt() } { e }
   }
 }
 
--- a/src/Pure/System/progress.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/progress.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -37,14 +37,14 @@
     Timing.timeit(message, enabled, echo)(e)
 
   @volatile protected var is_stopped = false
-  def stop: Unit = { is_stopped = true }
+  def stop(): Unit = { is_stopped = true }
   def stopped: Boolean =
   {
-    if (Thread.interrupted) is_stopped = true
+    if (Thread.interrupted()) is_stopped = true
     is_stopped
   }
 
-  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
+  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop() } { e }
   def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt()
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
--- a/src/Pure/System/scala.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/scala.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -114,7 +114,7 @@
             if (interpret) interp.interpret(source) == Results.Success
             else (new interp.ReadEvalPrint).compile(source)
           }
-        out.close
+        out.close()
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
@@ -195,7 +195,7 @@
 
     private def cancel(id: String, future: Future[Unit]): Unit =
     {
-      future.cancel
+      future.cancel()
       result(id, Scala.Tag.INTERRUPT, "")
     }
 
--- a/src/Pure/System/system_channel.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/system_channel.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -25,7 +25,7 @@
 
   override def toString: String = address
 
-  def shutdown(): Unit = server.close
+  def shutdown(): Unit = server.close()
 
   def rendezvous(): (OutputStream, InputStream) =
   {
@@ -36,8 +36,8 @@
 
       if (Byte_Message.read_line(in_stream).map(_.text) == Some(password)) (out_stream, in_stream)
       else {
-        out_stream.close
-        in_stream.close
+        out_stream.close()
+        in_stream.close()
         error("Failed to connect system channel: bad password")
       }
     }
--- a/src/Pure/System/tty_loop.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/System/tty_loop.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -30,7 +30,7 @@
         if (result.nonEmpty) {
           System.out.print(result.toString)
           System.out.flush()
-          result.clear
+          result.clear()
         }
         else {
           reader.close()
@@ -64,5 +64,5 @@
 
   def join: Unit = { console_output.join; console_input.join }
 
-  def cancel: Unit = console_input.cancel
+  def cancel(): Unit = console_input.cancel()
 }
--- a/src/Pure/Thy/file_format.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Thy/file_format.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -41,13 +41,13 @@
     def prover_options(options: Options): Options =
       agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
 
-    def stop_session: Unit = agents.foreach(_.stop)
+    def stop_session: Unit = agents.foreach(_.stop())
   }
 
   trait Agent
   {
     def prover_options(options: Options): Options = options
-    def stop: Unit = {}
+    def stop(): Unit = {}
   }
 
   object No_Agent extends Agent
--- a/src/Pure/Thy/sessions.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -1214,7 +1214,7 @@
   {
     def cache: XML.Cache = store.cache
 
-    def close: Unit = database_server.foreach(_.close)
+    def close(): Unit = database_server.foreach(_.close())
 
     def output_database[A](session: String)(f: SQL.Database => A): A =
       database_server match {
@@ -1350,7 +1350,7 @@
     def try_open_database(name: String, output: Boolean = false): Option[SQL.Database] =
     {
       def check(db: SQL.Database): Option[SQL.Database] =
-        if (output || session_info_exists(db)) Some(db) else { db.close; None }
+        if (output || session_info_exists(db)) Some(db) else { db.close(); None }
 
       if (database_server) check(open_database_server())
       else if (output) Some(SQLite.open_database(output_database(name)))
@@ -1380,7 +1380,7 @@
                   init_session_info(db, name)
                   relevant_db
                 }
-              } finally { db.close }
+              } finally { db.close() }
             case None => false
           }
         }
@@ -1420,16 +1420,16 @@
       db.transaction {
         db.create_table(Session_Info.table)
         db.using_statement(
-          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
+          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Export.Data.table)
         db.using_statement(
-          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
+          Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
 
         db.create_table(Presentation.Data.table)
         db.using_statement(
           Presentation.Data.table.delete(
-            Presentation.Data.session_name.where_equal(name)))(_.execute)
+            Presentation.Data.session_name.where_equal(name)))(_.execute())
       }
     }
 
--- a/src/Pure/Tools/build.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -60,7 +60,7 @@
             case exn: java.lang.Error => ignore_error(Exn.message(exn))
             case _: XML.Error => ignore_error("")
           }
-          finally { db.close }
+          finally { db.close() }
       }
     }
 
@@ -290,7 +290,7 @@
     }
 
     def sleep(): Unit =
-      Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
+      Isabelle_Thread.interrupt_handler(_ => progress.stop()) { Time.seconds(0.5).sleep }
 
     val numa_nodes = new NUMA.Nodes(numa_shuffling)
 
@@ -306,7 +306,7 @@
       if (pending.is_empty) results
       else {
         if (progress.stopped) {
-          for ((_, (_, job)) <- running) job.terminate
+          for ((_, (_, job)) <- running) job.terminate()
         }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
--- a/src/Pure/Tools/build_job.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -253,7 +253,7 @@
         private val promise: Promise[List[String]] = Future.promise
 
         def result: Exn.Result[List[String]] = promise.join_result
-        def cancel: Unit = promise.cancel
+        def cancel(): Unit = promise.cancel()
         def apply(errs: List[String]): Unit =
         {
           try { promise.fulfill(errs) }
@@ -286,7 +286,7 @@
 
       session.init_protocol_handler(new Session.Protocol_Handler
         {
-          override def exit(): Unit = Build_Session_Errors.cancel
+          override def exit(): Unit = Build_Session_Errors.cancel()
 
           private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
           {
@@ -416,8 +416,8 @@
           cwd = info.dir.file, env = env)
 
       val build_errors =
-        Isabelle_Thread.interrupt_handler(_ => process.terminate) {
-          Exn.capture { process.await_startup } match {
+        Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
+          Exn.capture { process.await_startup() } match {
             case Exn.Res(_) =>
               val resources_yxml = resources.init_session_yxml
               val args_yxml =
@@ -434,7 +434,7 @@
         }
 
       val process_result =
-        Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
+        Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() }
 
       session.stop()
 
@@ -502,13 +502,13 @@
       }
     }
 
-  def terminate: Unit = future_result.cancel
+  def terminate(): Unit = future_result.cancel()
   def is_finished: Boolean = future_result.is_finished
 
   private val timeout_request: Option[Event_Timer.Request] =
   {
     if (info.timeout > Time.zero)
-      Some(Event_Timer.request(Time.now() + info.timeout) { terminate })
+      Some(Event_Timer.request(Time.now() + info.timeout) { terminate() })
     else None
   }
 
@@ -519,7 +519,7 @@
     val was_timeout =
       timeout_request match {
         case None => false
-        case Some(request) => !request.cancel
+        case Some(request) => !request.cancel()
       }
 
     val result2 =
--- a/src/Pure/Tools/server.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Tools/server.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -149,9 +149,9 @@
         }
       }
 
-    def start: Unit = thread
+    def start(): Unit = thread
     def join: Unit = thread.join
-    def stop: Unit = { socket.close; join }
+    def stop(): Unit = { socket.close(); join }
   }
 
 
@@ -167,7 +167,7 @@
   {
     override def toString: String = socket.toString
 
-    def close(): Unit = socket.close
+    def close(): Unit = socket.close()
 
     def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
 
@@ -250,11 +250,11 @@
       _tasks.change(_ - task)
 
     def cancel_task(id: UUID.T): Unit =
-      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
+      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel()); tasks })
 
     def close(): Unit =
     {
-      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
+      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel()); (tasks.nonEmpty, tasks) }))
       { _tasks.value.foreach(_.join) }
     }
   }
@@ -293,7 +293,7 @@
     val ident: JSON.Object.Entry = ("task" -> id.toString)
 
     val progress: Connection_Progress = context.progress(ident)
-    def cancel: Unit = progress.stop
+    def cancel(): Unit = progress.stop()
 
     private lazy val thread = Isabelle_Thread.fork(name = "server_task")
     {
@@ -304,7 +304,7 @@
           val err = json_error(exn)
           if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
       }
-      progress.stop
+      progress.stop()
       context.remove_task(task)
     }
     def start: Unit = thread
@@ -351,7 +351,7 @@
       connection
     }
 
-    def active(): Boolean =
+    def active: Boolean =
       try {
         using(connection())(connection =>
           {
@@ -411,7 +411,7 @@
           db.create_table(Data.table)
           list(db).filterNot(_.active).foreach(server_info =>
             db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
-              _.execute))
+              _.execute()))
         }
         db.transaction {
           find(db, name) match {
@@ -422,7 +422,7 @@
               val server = new Server(port, log)
               val server_info = Info(name, server.port, server.password)
 
-              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
               db.using_statement(Data.table.insert())(stmt =>
               {
                 stmt.string(1) = server_info.name
@@ -431,7 +431,7 @@
                 stmt.execute()
               })
 
-              server.start
+              server.start()
               (server_info, Some(server))
           }
         }
@@ -534,7 +534,7 @@
 
   def shutdown(): Unit =
   {
-    server.socket.close
+    server.socket.close()
 
     val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
     for ((_, session) <- sessions) {
--- a/src/Pure/Tools/spell_checker.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -88,7 +88,7 @@
     }
   }
 
-  def dictionaries(): List[Dictionary] =
+  def dictionaries: List[Dictionary] =
     for {
       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
       if path.is_file
--- a/src/Tools/Graphview/graph_panel.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -341,8 +341,8 @@
     tooltip = "Use editor font and colors for painting"
   }
 
-  private val colorations = new Button { action = Action("Colorations") { color_dialog.open } }
-  private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
+  private val colorations = new Button { action = Action("Colorations") { color_dialog.open() } }
+  private val filters = new Button { action = Action("Filters") { mutator_dialog.open() } }
 
   private val controls =
     Wrap_Panel(
--- a/src/Tools/Graphview/mutator_dialog.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -46,7 +46,7 @@
   override def open(): Unit =
   {
     if (!visible) panels = get_panels(container())
-    super.open
+    super.open()
   }
 
   minimumSize = new Dimension(700, 200)
@@ -94,8 +94,8 @@
 
   def paint_panels(): Unit =
   {
-    Focus_Traveral_Policy.clear
-    filter_panel.contents.clear
+    Focus_Traveral_Policy.clear()
+    filter_panel.contents.clear()
     panels.map(x => {
         filter_panel.contents += x
         Focus_Traveral_Policy.addAll(x.focusList)
@@ -106,8 +106,8 @@
     Focus_Traveral_Policy.add(add_button.peer)
     Focus_Traveral_Policy.add(apply_button.peer)
     Focus_Traveral_Policy.add(cancel_button.peer)
-    filter_panel.revalidate
-    filter_panel.repaint
+    filter_panel.revalidate()
+    filter_panel.repaint()
   }
 
   val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
@@ -130,7 +130,7 @@
   }
 
   private val cancel_button = new Button {
-    action = Action("Close") { close }
+    action = Action("Close") { close() }
   }
   defaultButton = cancel_button
 
--- a/src/Tools/VSCode/src/language_server.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -136,7 +136,7 @@
       val (invoke_input, invoke_load) =
         resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
-      if (invoke_load) delay_load.invoke
+      if (invoke_load) delay_load.invoke()
     }
 
   private val file_watcher =
@@ -307,7 +307,7 @@
 
       try {
         Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options),
-          modes = modes, logic = base_info.session).await_startup
+          modes = modes, logic = base_info.session).await_startup()
         reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")")
       }
       catch { case ERROR(msg) => reply_error(msg) }
--- a/src/Tools/jEdit/src-base/jedit_lib.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -19,7 +19,7 @@
     val view = if (alt_view != null) alt_view else jEdit.getActiveView()
     if (view != null) {
       val text_area = view.getTextArea
-      if (text_area != null) text_area.requestFocus
+      if (text_area != null) text_area.requestFocus()
     }
   }
 }
\ No newline at end of file
--- a/src/Tools/jEdit/src/active.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/active.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -95,7 +95,7 @@
                   Isabelle.insert_line_padding(text_area, text)
                 else text_area.setSelectedText(text)
             }
-            text_area.requestFocus
+            text_area.requestFocus()
           }
           true
 
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -281,7 +281,7 @@
               {
                 if (view.getKeyEventInterceptor == inner_key_listener)
                   view.setKeyEventInterceptor(null)
-                if (focus) text_area.requestFocus
+                if (focus) text_area.requestFocus()
                 JEdit_Lib.invalidate_range(text_area, range)
               }
             }
@@ -501,7 +501,7 @@
                   override def propagate(evt: KeyEvent): Unit =
                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
                   override def shutdown(focus: Boolean): Unit =
-                    if (focus) text_field.requestFocus
+                    if (focus) text_field.requestFocus()
                 }
               dismissed()
               completion_popup = Some(completion)
@@ -703,7 +703,7 @@
   private def show_popup(focus: Boolean): Unit =
   {
     popup.show
-    if (focus) list_view.requestFocus
+    if (focus) list_view.requestFocus()
   }
 
   private def hide_popup(): Unit =
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -298,7 +298,7 @@
 
   /* focus */
 
-  override def focusOnDefaultComponent(): Unit = eval_button.requestFocus
+  override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()
 
   addFocusListener(new FocusAdapter {
     override def focusGained(e: FocusEvent): Unit = update_focus()
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -592,7 +592,7 @@
         val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
-          pending.clear
+          pending.clear()
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -616,5 +616,5 @@
   /* java monitor */
 
   def java_monitor(view: View): Unit =
-    Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf())
+    Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf)
 }
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -180,7 +180,7 @@
   {
     val opt_snapshot =
       Document_Model.get(buffer) match {
-        case Some(model) if model.is_theory => Some(model.snapshot)
+        case Some(model) if model.is_theory => Some(model.snapshot())
         case _ => None
       }
     opt_snapshot match {
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -66,7 +66,7 @@
   {
     GUI_Thread.require {}
     Document_Model.get(name) match {
-      case Some(model) => model.snapshot
+      case Some(model) => model.snapshot()
       case None => session.snapshot(name)
     }
   }
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -50,7 +50,7 @@
 
     dummy_window.setContentPane(outer)
     dummy_window.pack
-    dummy_window.revalidate
+    dummy_window.revalidate()
 
     val geometry =
       Window_Geometry(
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -18,10 +18,10 @@
 {
   /* session options */
 
-  def session_dirs(): List[Path] =
+  def session_dirs: List[Path] =
     Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
 
-  def session_no_build(): Boolean =
+  def session_no_build: Boolean =
     Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
 
   def session_options(options: Options): Options =
@@ -41,7 +41,7 @@
     options2
   }
 
-  def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
+  def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure =
     Sessions.load_structure(session_options(options), dirs = dirs)
 
 
@@ -119,7 +119,7 @@
 
   def session_base_info(options: Options): Sessions.Base_Info =
     Sessions.base_info(options,
-      dirs = JEdit_Sessions.session_dirs(),
+      dirs = JEdit_Sessions.session_dirs,
       include_sessions = logic_include_sessions,
       session = logic_name(options),
       session_ancestor = logic_ancestor,
@@ -130,7 +130,7 @@
   {
     Build.build(session_options(options),
       selection = Sessions.Selection.session(PIDE.resources.session_name),
-      progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs(),
+      progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
       infos = PIDE.resources.session_base_info.infos).rc
   }
 
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -87,7 +87,7 @@
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    val entries = Spell_Checker.dictionaries()
+    val entries = Spell_Checker.dictionaries
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
       val title = opt.title()
--- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -29,7 +29,7 @@
   def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
   {
     val buffer = JEdit_Lib.jedit_view(view).getBuffer
-    Document_Model.get(buffer).map(_.snapshot)
+    Document_Model.get(buffer).map(_.snapshot())
   }
 
   def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
@@ -393,7 +393,7 @@
 
         case msg: PropertiesChanged =>
           for {
-            view <- JEdit_Lib.jedit_views
+            view <- JEdit_Lib.jedit_views()
             edit_pane <- JEdit_Lib.jedit_edit_panes(view)
           } {
             val buffer = edit_pane.getBuffer
@@ -458,13 +458,13 @@
       completion_history.load()
       spell_checker.update(options.value)
 
-      JEdit_Lib.jedit_views.foreach(init_title)
+      JEdit_Lib.jedit_views().foreach(init_title)
 
       isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
       init_mode_provider()
-      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init)
+      JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
 
-      http_server.start
+      http_server.start()
 
       startup_failure = None
     }
@@ -483,11 +483,11 @@
 
   override def stop(): Unit =
   {
-    http_server.stop
+    http_server.stop()
 
     isabelle.jedit_base.Syntax_Style.dummy_style_extender()
     exit_mode_provider()
-    JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit)
+    JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
 
     if (startup_failure.isEmpty) {
       options.value.save_prefs()
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -95,7 +95,7 @@
       val results = current_base_results
       val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
 
-      future_refresh.foreach(_.cancel)
+      future_refresh.foreach(_.cancel())
       future_refresh =
         Some(Future.fork {
           val (text, rendering) =
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -280,12 +280,12 @@
   private def show_popup: Unit =
   {
     popup.show
-    pretty_text_area.requestFocus
+    pretty_text_area.requestFocus()
     pretty_text_area.update(rendering.snapshot, results, info.info)
   }
 
   private def hide_popup: Unit = popup.hide
 
-  private def request_focus: Unit = pretty_text_area.requestFocus
+  private def request_focus: Unit = pretty_text_area.requestFocus()
 }
 
--- a/src/Tools/jEdit/src/process_indicator.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/process_indicator.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -34,7 +34,7 @@
         {
           current_frame = (current_frame + 1) % active_icons.length
           setImage(active_icons(current_frame))
-          label.repaint
+          label.repaint()
         }
       })
     timer.setRepeats(true)
@@ -44,7 +44,7 @@
       if (rate == 0) {
         setImage(passive_icon)
         timer.stop
-        label.repaint
+        label.repaint()
       }
       else {
         val delay = 1000 / rate
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -258,7 +258,7 @@
 
     def select: Unit =
     {
-      control_panel.contents.clear
+      control_panel.contents.clear()
       control_panel.contents += query_label
       update_items().foreach(item => control_panel.contents += item.checkbox)
       control_panel.contents ++=
@@ -291,13 +291,13 @@
 
   private def select_operation(): Unit =
   {
-    for (op <- get_operation()) { op.select; op.query.requestFocus }
-    operations_pane.revalidate
+    for (op <- get_operation()) { op.select; op.query.requestFocus() }
+    operations_pane.revalidate()
   }
 
   override def focusOnDefaultComponent(): Unit =
   {
-    for (op <- get_operation()) op.query.requestFocus
+    for (op <- get_operation()) op.query.requestFocus()
   }
 
   select_operation()
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -221,7 +221,7 @@
                 case _: ArrayIndexOutOfBoundsException =>
                 case _: IllegalArgumentException =>
               }
-              text_area.requestFocus
+              text_area.requestFocus()
             }
             link.follow(view)
           case None =>
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -30,7 +30,7 @@
 
     override def flush(): Unit =
     {
-      val s = buf.synchronized { val s = buf.toString; buf.clear; s }
+      val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
       val str = UTF8.decode_permissive(s)
       GUI_Thread.later {
         if (global_out == null) System.out.print(str)
@@ -97,7 +97,7 @@
   private class Interpreter
   {
     private val running = Synchronized[Option[Thread]](None)
-    def interrupt: Unit = running.change(opt => { opt.foreach(_.interrupt); opt })
+    def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
 
     private val interp =
       Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
@@ -146,8 +146,8 @@
   {
     interpreters.get(console) match {
       case Some(interp) =>
-        interp.interrupt
-        interp.thread.shutdown
+        interp.interrupt()
+        interp.thread.shutdown()
         interpreters -= console
       case None =>
     }
@@ -177,5 +177,5 @@
   }
 
   override def stop(console: Console): Unit =
-    interpreters.get(console).foreach(_.interrupt)
+    interpreters.get(console).foreach(_.interrupt())
 }
--- a/src/Tools/jEdit/src/session_build.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -80,10 +80,10 @@
 
     private def set_actions(cs: Component*): Unit =
     {
-      action_panel.contents.clear
+      action_panel.contents.clear()
       action_panel.contents ++= cs
-      layout_panel.revalidate
-      layout_panel.repaint
+      layout_panel.revalidate()
+      layout_panel.repaint()
     }
 
 
@@ -94,7 +94,7 @@
     private def return_code(rc: Int): Unit =
       GUI_Thread.later {
         _return_code = Some(rc)
-        delay_exit.invoke
+        delay_exit.invoke()
       }
 
     private val delay_exit =
@@ -129,7 +129,7 @@
 
     private def stopping(): Unit =
     {
-      progress.stop
+      progress.stop()
       set_actions(new Label("Stopping ..."))
     }
 
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -145,7 +145,7 @@
 
   add(controls.peer, BorderLayout.NORTH)
 
-  override def focusOnDefaultComponent(): Unit = provers.requestFocus
+  override def focusOnDefaultComponent(): Unit = provers.requestFocus()
 
 
   /* main */
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -43,7 +43,7 @@
           Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
         text_area.setSelectedText(s1 + s2)
         text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
-        text_area.requestFocus
+        text_area.requestFocus()
       }
     tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
   }
@@ -67,12 +67,12 @@
                 forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
             } yield (txt, abbr)): _*).iterator_list.toList
 
-        contents.clear
+        contents.clear()
         for ((txt, abbrs) <- entries.sortBy(_._1))
           contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
 
-        revalidate
-        repaint
+        revalidate()
+        repaint()
       }
     }
 
@@ -101,7 +101,7 @@
           Syntax_Style.edit_control_style(text_area, symbol)
         else
           text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
-        text_area.requestFocus
+        text_area.requestFocus()
       }
     tooltip =
       GUI.tooltip_lines(
@@ -113,7 +113,7 @@
     action = Action("Reset") {
       val text_area = view.getTextArea
       Syntax_Style.edit_control_style(text_area, "")
-      text_area.requestFocus
+      text_area.requestFocus()
     }
     tooltip = "Reset control symbols within text"
   }
@@ -135,14 +135,14 @@
         val results =
           for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
 
-        results_panel.contents.clear
+        results_panel.contents.clear()
         for (sym <- results.take(search_limit))
           results_panel.contents += new Symbol_Component(sym, false)
         if (results.length > search_limit)
           results_panel.contents +=
             new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
-        revalidate
-        repaint
+        revalidate()
+        repaint()
       }
       search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
   }
@@ -170,7 +170,7 @@
     listenTo(selection)
     reactions += {
       case SelectionChanged(_) if selection.page == search_page =>
-        search_panel.search_field.requestFocus
+        search_panel.search_field.requestFocus()
     }
 
     for (page <- pages)
--- a/src/Tools/jEdit/src/text_overview.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -116,7 +116,7 @@
   private def is_running(): Boolean = !future_refresh.value.is_finished
 
   def invoke(): Unit = delay_refresh.invoke()
-  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
+  def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel(); x }) }
 
   private val delay_refresh =
     Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
--- a/src/Tools/jEdit/src/text_structure.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -93,7 +93,7 @@
                   (for {
                     text_area <- JEdit_Lib.jedit_text_areas(buffer)
                     doc_view <- Document_View.get(text_area)
-                  } yield doc_view.get_rendering).nextOption()
+                  } yield doc_view.get_rendering()).nextOption()
                 }
               else None
             val limit = PIDE.options.value.int("jedit_indent_script_limit")