# HG changeset patch # User wenzelm # Date 1614888267 -3600 # Node ID 77ef8bef0593a844435cd7c67493b8579ab7840e # Parent 5f388e514ab800c6c674d406f4060d7138fc0cb2 clarified signature --- fewer warnings; diff -r 5f388e514ab8 -r 77ef8bef0593 src/HOL/Tools/Nitpick/kodkod.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") diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Concurrent/delay.scala --- 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 => diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Concurrent/event_timer.scala --- 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 = diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Concurrent/future.scala --- 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() } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Concurrent/isabelle_thread.scala --- 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() } } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Concurrent/par_list.scala --- 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) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/GUI/gui.scala --- 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 { diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/exn.scala --- 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 } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/file.scala --- 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 } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/file_watcher.scala --- 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() } } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/http.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/mailman.scala --- 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() } }) } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/scan.scala --- 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) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/sql.scala --- 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()) } } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/ssh.scala --- 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) diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/General/url.scala --- 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 } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Isar/outer_syntax.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/ML/ml_console.scala --- 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) diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/ML/ml_statistics.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/PIDE/headless.scala --- 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 } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/PIDE/prover.scala --- 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") } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/PIDE/session.scala --- 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) => diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/bash.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/isabelle_process.scala --- 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() } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/isabelle_system.scala --- 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) diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/isabelle_tool.scala --- 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) diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/posix_interrupt.scala --- 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 } } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/progress.scala --- 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" diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/scala.scala --- 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, "") } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/system_channel.scala --- 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") } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/System/tty_loop.scala --- 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() } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Thy/file_format.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Thy/sessions.scala --- 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()) } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Tools/build.scala --- 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 { diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Tools/build_job.scala --- 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 = diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Tools/server.scala --- 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) { diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/Tools/spell_checker.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/Graphview/graph_panel.scala --- 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( diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/Graphview/mutator_dialog.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/VSCode/src/language_server.scala --- 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) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src-base/jedit_lib.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/active.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/completion_popup.scala --- 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 = diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/debugger_dockable.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/document_model.scala --- 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) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/isabelle.scala --- 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) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 { diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/jedit_editor.scala --- 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) } } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/jedit_lib.scala --- 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( diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/jedit_sessions.scala --- 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 } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/jedit_spell_checker.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/plugin.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/pretty_text_area.scala --- 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) = diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/pretty_tooltip.scala --- 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() } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/process_indicator.scala --- 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 diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/query_dockable.scala --- 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() diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/rich_text_area.scala --- 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 => diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/scala_console.scala --- 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()) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/session_build.scala --- 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 ...")) } diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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 */ diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/symbols_dockable.scala --- 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) diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/text_overview.scala --- 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) { diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src/text_structure.scala --- 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")