--- 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")