--- a/src/Pure/Admin/afp.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/afp.scala Mon Mar 01 22:22:12 2021 +0100
@@ -90,7 +90,7 @@
val Extra_Line = """^\s+(.*)$""".r
val Blank_Line = """^\s*$""".r
- def flush()
+ def flush(): Unit =
{
if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty))
section = ""
--- a/src/Pure/Admin/build_csdp.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala Mon Mar 01 22:22:12 2021 +0100
@@ -26,7 +26,7 @@
Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2)
.mkString("\n"))
- def change(path: Path)
+ def change(path: Path): Unit =
{
def change_line(line: String, entry: (String, String)): String =
line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
@@ -56,7 +56,7 @@
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current,
- mingw: MinGW = MinGW.none)
+ mingw: MinGW = MinGW.none): Unit =
{
mingw.check
--- a/src/Pure/Admin/build_cygwin.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Mon Mar 01 22:22:12 2021 +0100
@@ -16,7 +16,7 @@
def build_cygwin(progress: Progress,
mirror: String = default_mirror,
- more_packages: List[String] = Nil)
+ more_packages: List[String] = Nil): Unit =
{
require(Platform.is_windows, "Windows platform expected")
--- a/src/Pure/Admin/build_doc.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_doc.scala Mon Mar 01 22:22:12 2021 +0100
@@ -16,7 +16,7 @@
progress: Progress = new Progress,
all_docs: Boolean = false,
max_jobs: Int = 1,
- docs: List[String] = Nil)
+ docs: List[String] = Nil): Unit =
{
val store = Sessions.store(options)
--- a/src/Pure/Admin/build_e.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_e.scala Mon Mar 01 22:22:12 2021 +0100
@@ -19,7 +19,7 @@
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
--- a/src/Pure/Admin/build_fonts.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_fonts.scala Mon Mar 01 22:22:12 2021 +0100
@@ -179,7 +179,7 @@
/* hinting */
// see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
- private def auto_hint(source: Path, target: Path)
+ private def auto_hint(source: Path, target: Path): Unit =
{
Isabelle_System.bash("ttfautohint -i " +
File.bash_path(source) + " " + File.bash_path(target)).check
@@ -216,7 +216,7 @@
target_prefix: String = "Isabelle",
target_version: String = "",
target_dir: Path = default_target_dir,
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
progress.echo("Directory " + target_dir)
hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted)))
--- a/src/Pure/Admin/build_history.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_history.scala Mon Mar 01 22:22:12 2021 +0100
@@ -399,7 +399,7 @@
}
}
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev: Option[String] = None
--- a/src/Pure/Admin/build_jdk.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_jdk.scala Mon Mar 01 22:22:12 2021 +0100
@@ -152,7 +152,7 @@
def build_jdk(
archives: List[Path],
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
if (Platform.is_windows) error("Cannot build jdk on Windows")
--- a/src/Pure/Admin/build_log.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_log.scala Mon Mar 01 22:22:12 2021 +0100
@@ -874,7 +874,8 @@
ssh_close = true)
}
- def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
+ def update_database(
+ db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false): Unit =
{
val log_files =
dirs.flatMap(dir =>
@@ -887,7 +888,7 @@
}
def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
- days: Int = 100, ml_statistics: Boolean = false)
+ days: Int = 100, ml_statistics: Boolean = false): Unit =
{
Isabelle_System.make_directory(sqlite_database.dir)
sqlite_database.file.delete
@@ -952,7 +953,7 @@
db.using_statement(table.select(List(column), distinct = true))(stmt =>
stmt.execute_query().iterator(_.string(column)).toSet)
- def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
+ def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
{
val table = Data.meta_info_table
db.using_statement(db.insert_permissive(table))(stmt =>
@@ -968,7 +969,7 @@
})
}
- def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info)
+ def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
{
val table = Data.sessions_table
db.using_statement(db.insert_permissive(table))(stmt =>
@@ -999,7 +1000,7 @@
})
}
- def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info)
+ def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
{
val table = Data.theories_table
db.using_statement(db.insert_permissive(table))(stmt =>
@@ -1023,7 +1024,7 @@
})
}
- def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info)
+ def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
{
val table = Data.ml_statistics_table
db.using_statement(db.insert_permissive(table))(stmt =>
@@ -1042,7 +1043,7 @@
})
}
- def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)
+ def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false): Unit =
{
abstract class Table_Status(table: SQL.Table)
{
@@ -1052,7 +1053,7 @@
def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
def update_db(db: SQL.Database, log_file: Log_File): Unit
- def update(log_file: Log_File)
+ def update(log_file: Log_File): Unit =
{
if (!known(log_file.name)) {
update_db(db, log_file)
--- a/src/Pure/Admin/build_polyml.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_polyml.scala Mon Mar 01 22:22:12 2021 +0100
@@ -45,7 +45,7 @@
progress: Progress = new Progress,
arch_64: Boolean = false,
options: List[String] = Nil,
- mingw: MinGW = MinGW.none)
+ mingw: MinGW = MinGW.none): Unit =
{
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
error("Bad Poly/ML root directory: " + root)
@@ -147,7 +147,7 @@
/** skeleton for component **/
- private def extract_sources(source_archive: Path, component_dir: Path)
+ private def extract_sources(source_archive: Path, component_dir: Path): Unit =
{
if (source_archive.get_ext == "zip") {
Isabelle_System.bash(
@@ -182,7 +182,7 @@
def build_polyml_component(
source_archive: Path,
component_dir: Path,
- sha1_root: Option[Path] = None)
+ sha1_root: Option[Path] = None): Unit =
{
Isabelle_System.new_directory(component_dir)
extract_sources(source_archive, component_dir)
--- a/src/Pure/Admin/build_release.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_release.scala Mon Mar 01 22:22:12 2021 +0100
@@ -54,7 +54,7 @@
private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
- def patch_release(release: Release, is_official: Boolean)
+ def patch_release(release: Release, is_official: Boolean): Unit =
{
val dir = release.isabelle_dir
@@ -89,7 +89,7 @@
/* ANNOUNCE */
- def make_announce(release: Release)
+ def make_announce(release: Release): Unit =
{
File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
"""
@@ -104,7 +104,7 @@
/* NEWS */
- def make_news(other_isabelle: Other_Isabelle, dist_version: String)
+ def make_news(other_isabelle: Other_Isabelle, dist_version: String): Unit =
{
val target = other_isabelle.isabelle_home + Path.explode("doc")
val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
@@ -140,7 +140,7 @@
}
}
- def record_bundled_components(dir: Path)
+ def record_bundled_components(dir: Path): Unit =
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
@@ -172,7 +172,8 @@
(components, jdk_component)
}
- def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
+ def activate_components(
+ dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
@@ -188,7 +189,7 @@
}) ::: more_names.map(contrib_name))
}
- def make_contrib(dir: Path)
+ def make_contrib(dir: Path): Unit =
{
Isabelle_System.make_directory(Components.contrib(dir))
File.write(Components.contrib(dir, "README"),
@@ -215,7 +216,7 @@
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
- local_dir: Path)
+ local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
options.string(server_option) match {
@@ -248,7 +249,7 @@
/* Isabelle application */
- def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n")
+ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
@@ -260,7 +261,7 @@
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
- dock_icon: Boolean = false)
+ dock_icon: Boolean = false): Unit =
{
val script = """#!/usr/bin/env bash
#
@@ -309,7 +310,7 @@
}
- def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String)
+ def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
{
File.write(path, """<?xml version="1.0" ?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
@@ -852,7 +853,7 @@
/** command line entry point **/
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev = ""
--- a/src/Pure/Admin/build_spass.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_spass.scala Mon Mar 01 22:22:12 2021 +0100
@@ -18,7 +18,7 @@
download_url: String = default_download_url,
verbose: Boolean = false,
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
--- a/src/Pure/Admin/build_sqlite.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Mon Mar 01 22:22:12 2021 +0100
@@ -14,7 +14,7 @@
def build_sqlite(
download_url: String,
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
val Download_Name = """^.*/([^/]+)\.jar""".r
val download_name =
--- a/src/Pure/Admin/build_status.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Mon Mar 01 22:22:12 2021 +0100
@@ -55,7 +55,7 @@
verbose: Boolean = false,
target_dir: Path = default_target_dir,
ml_statistics: Boolean = false,
- image_size: (Int, Int) = default_image_size)
+ image_size: (Int, Int) = default_image_size): Unit =
{
val ml_statistics_domain =
Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields,
@@ -363,7 +363,7 @@
def present_data(data: Data,
progress: Progress = new Progress,
target_dir: Path = default_target_dir,
- image_size: (Int, Int) = default_image_size)
+ image_size: (Int, Int) = default_image_size): Unit =
{
def clean_name(name: String): String =
name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
--- a/src/Pure/Admin/build_vampire.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_vampire.scala Mon Mar 01 22:22:12 2021 +0100
@@ -27,7 +27,7 @@
component_name: String = "",
verbose: Boolean = false,
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
Isabelle_System.require_command("git", "cmake")
--- a/src/Pure/Admin/build_verit.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_verit.scala Mon Mar 01 22:22:12 2021 +0100
@@ -19,7 +19,7 @@
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current,
- mingw: MinGW = MinGW.none)
+ mingw: MinGW = MinGW.none): Unit =
{
mingw.check
--- a/src/Pure/Admin/build_zipperposition.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala Mon Mar 01 22:22:12 2021 +0100
@@ -18,7 +18,7 @@
version: String = default_version,
verbose: Boolean = false,
progress: Progress = new Progress,
- target_dir: Path = Path.current)
+ target_dir: Path = Path.current): Unit =
{
Isabelle_System.with_tmp_dir("build")(build_dir =>
{
--- a/src/Pure/Admin/check_sources.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/check_sources.scala Mon Mar 01 22:22:12 2021 +0100
@@ -9,7 +9,7 @@
object Check_Sources
{
- def check_file(path: Path)
+ def check_file(path: Path): Unit =
{
val file_name = path.implode
val file_pos = path.position
@@ -49,7 +49,7 @@
Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
}
- def check_hg(root: Path)
+ def check_hg(root: Path): Unit =
{
Output.writeln("Checking " + root + " ...")
val hg = Mercurial.repository(root)
--- a/src/Pure/Admin/components.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/components.scala Mon Mar 01 22:22:12 2021 +0100
@@ -59,7 +59,7 @@
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
Isabelle_System.make_directory(base_dir)
for (name <- names) {
@@ -78,7 +78,7 @@
}
}
- def purge(dir: Path, platform: Platform.Family.Value)
+ def purge(dir: Path, platform: Platform.Family.Value): Unit =
{
def purge_platforms(platforms: String*): Set[String] =
platforms.flatMap(name =>
@@ -191,7 +191,7 @@
progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
- update_components_sha1: Boolean = false)
+ update_components_sha1: Boolean = false): Unit =
{
val archives: List[Path] =
for (path <- components) yield {
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 01 22:22:12 2021 +0100
@@ -441,7 +441,7 @@
true
})
- def shutdown() { thread.shutdown() }
+ def shutdown(): Unit = { thread.shutdown() }
val hostname: String = Isabelle_System.hostname()
@@ -453,7 +453,7 @@
def start_logger(start_date: Date, task_name: String): Logger =
new Logger(this, start_date, task_name)
- def run_task(start_date: Date, task: Logger_Task)
+ def run_task(start_date: Date, task: Logger_Task): Unit =
{
val logger = start_logger(start_date, task.name)
val res = Exn.capture { task.body(logger) }
@@ -482,7 +482,7 @@
def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
- def log_end(end_date: Date, err: Option[String])
+ def log_end(end_date: Date, err: Option[String]): Unit =
{
val elapsed_time = end_date.time - start_date.time
val msg =
@@ -506,7 +506,7 @@
/** cronjob **/
- def cronjob(progress: Progress, exclude_task: Set[String])
+ def cronjob(progress: Progress, exclude_task: Set[String]): Unit =
{
/* soft lock */
@@ -525,9 +525,9 @@
val log_service = Log_Service(Options.init(), progress = progress)
- def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
+ def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task)
- def run_now(task: Logger_Task) { run(Date.now(), task) }
+ def run_now(task: Logger_Task): Unit = run(Date.now(), task)
/* structured tasks */
@@ -538,7 +538,7 @@
def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
{
- @tailrec def join(running: List[Task])
+ @tailrec def join(running: List[Task]): Unit =
{
running.partition(_.is_finished) match {
case (Nil, Nil) =>
@@ -604,7 +604,7 @@
/** command line entry point **/
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
var force = false
--- a/src/Pure/Admin/isabelle_devel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -20,7 +20,7 @@
/* index */
- def make_index()
+ def make_index(): Unit =
{
val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
@@ -38,7 +38,7 @@
options: Options,
rev: String = "",
afp_rev: String = "",
- parallel_jobs: Int = 1)
+ parallel_jobs: Int = 1): Unit =
{
Isabelle_System.with_tmp_dir("isadist")(base_dir =>
{
@@ -54,7 +54,7 @@
/* maintain build_log database */
- def build_log_database(options: Options, log_dirs: List[Path])
+ def build_log_database(options: Options, log_dirs: List[Path]): Unit =
{
val store = Build_Log.store(options)
using(store.open_database())(db =>
@@ -68,7 +68,7 @@
/* present build status */
- def build_status(options: Options)
+ def build_status(options: Options): Unit =
{
Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS),
dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true))
--- a/src/Pure/Admin/jenkins.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/jenkins.scala Mon Mar 01 22:22:12 2021 +0100
@@ -40,7 +40,7 @@
def download_logs(
- options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress)
+ options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress): Unit =
{
val store = Sessions.store(options)
val infos = job_names.flatMap(build_job_infos)
@@ -96,7 +96,7 @@
}
}
- def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress)
+ def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress): Unit =
{
val log_dir = dir + Build_Log.log_subdir(date)
val log_path = log_dir + log_filename.xz
--- a/src/Pure/Admin/other_isabelle.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Mon Mar 01 22:22:12 2021 +0100
@@ -96,7 +96,7 @@
}
else false
- def init_settings(settings: List[String])
+ def init_settings(settings: List[String]): Unit =
{
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
@@ -111,7 +111,7 @@
/* cleanup */
- def cleanup()
+ def cleanup(): Unit =
{
clean_settings()
etc.file.delete
--- a/src/Pure/Concurrent/consumer_thread.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala Mon Mar 01 22:22:12 2021 +0100
@@ -66,7 +66,7 @@
val ack: Option[Synchronized[Option[Exn.Result[Unit]]]] =
if (acknowledge) Some(Synchronized(None)) else None
- def await
+ def await: Unit =
{
for (a <- ack) {
Exn.release(a.guarded_access({ case None => None case res => Some((res.get, res)) }))
@@ -74,7 +74,7 @@
}
}
- private def request(req: Request)
+ private def request(req: Request): Unit =
{
synchronized {
if (is_active) mailbox.send(Some(req))
@@ -113,10 +113,10 @@
assert(is_active)
- def send(arg: A) { request(new Request(arg)) }
- def send_wait(arg: A) { request(new Request(arg, acknowledge = true)) }
+ def send(arg: A): Unit = request(new Request(arg))
+ def send_wait(arg: A): Unit = request(new Request(arg, acknowledge = true))
- def shutdown()
+ def shutdown(): Unit =
{
synchronized { if (is_active) { active = false; mailbox.send(None) } }
thread.join
--- a/src/Pure/Concurrent/event_timer.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Concurrent/event_timer.scala Mon Mar 01 22:22:12 2021 +0100
@@ -24,7 +24,7 @@
def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request =
{
- val task = new TimerTask { def run { event } }
+ val task = new TimerTask { def run: Unit = event }
repeat match {
case None => event_timer.schedule(task, new JDate(time.ms))
case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms)
--- a/src/Pure/Concurrent/future.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Concurrent/future.scala Mon Mar 01 22:22:12 2021 +0100
@@ -61,7 +61,7 @@
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
def join_result: Exn.Result[A] = peek.get
- def cancel {}
+ def cancel: Unit = {}
}
@@ -83,7 +83,7 @@
case _ => None
}
- private def try_run()
+ private def try_run(): Unit =
{
val do_run =
status.change_result {
--- a/src/Pure/Concurrent/isabelle_thread.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Mon Mar 01 22:22:12 2021 +0100
@@ -107,7 +107,7 @@
class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String)
extends Function[Isabelle_Thread, Unit]
{
- def apply(thread: Isabelle_Thread) { handle(thread) }
+ def apply(thread: Isabelle_Thread): Unit = handle(thread)
override def toString: String = name
}
@@ -138,7 +138,7 @@
thread.setPriority(pri)
thread.setDaemon(daemon)
- override def run { main.run() }
+ override def run: Unit = main.run()
def is_self: Boolean = Thread.currentThread == thread
--- a/src/Pure/GUI/gui.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/GUI/gui.scala Mon Mar 01 22:22:12 2021 +0100
@@ -36,7 +36,7 @@
lazy val look_and_feels: List[Look_And_Feel] =
Isabelle_System.make_services(classOf[Look_And_Feel])
- def init_lafs()
+ def init_lafs(): Unit =
{
val old_lafs =
Set(
@@ -54,7 +54,7 @@
/* plain focus traversal, notably for text fields */
- def plain_focus_traversal(component: Component)
+ def plain_focus_traversal(component: Component): Unit =
{
val dummy_button = new JButton
def apply(id: Int): Unit =
@@ -78,7 +78,7 @@
}
private def simple_dialog(kind: Int, default_title: String,
- parent: Component, title: String, message: Iterable[Any])
+ parent: Component, title: String, message: Iterable[Any]): Unit =
{
GUI_Thread.now {
val java_message =
@@ -127,7 +127,8 @@
private def print(i: Int): String = i.toString + "%"
- def set_item(i: Int) {
+ def set_item(i: Int): Unit =
+ {
peer.getEditor match {
case null =>
case editor => editor.setItem(print(i))
@@ -272,9 +273,9 @@
case _ => None
}
- def traverse_components(component: Component, apply: Component => Unit)
+ def traverse_components(component: Component, apply: Component => Unit): Unit =
{
- def traverse(comp: Component)
+ def traverse(comp: Component): Unit =
{
apply(comp)
comp match {
@@ -326,7 +327,7 @@
"font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
}
- def use_isabelle_fonts()
+ def use_isabelle_fonts(): Unit =
{
val default_font = label_font()
val ui = UIManager.getDefaults
--- a/src/Pure/GUI/gui_thread.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/GUI/gui_thread.scala Mon Mar 01 22:22:12 2021 +0100
@@ -39,7 +39,7 @@
}
}
- def later(body: => Unit)
+ def later(body: => Unit): Unit =
{
if (SwingUtilities.isEventDispatchThread) body
else SwingUtilities.invokeLater(() => body)
--- a/src/Pure/GUI/popup.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/GUI/popup.scala Mon Mar 01 22:22:12 2021 +0100
@@ -17,7 +17,7 @@
location: Point,
size: Dimension)
{
- def show
+ def show: Unit =
{
component.setLocation(location)
component.setSize(size)
@@ -28,7 +28,7 @@
layered.repaint(component.getBounds())
}
- def hide
+ def hide: Unit =
{
val bounds = component.getBounds()
layered.remove(component)
--- a/src/Pure/GUI/wrap_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/GUI/wrap_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -53,7 +53,7 @@
val dim = new Dimension(0, 0)
var row_width = 0
var row_height = 0
- def add_row()
+ def add_row(): Unit =
{
dim.width = dim.width max row_width
if (dim.height > 0) dim.height += vgap
@@ -118,7 +118,7 @@
private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]
def vGap: Int = layoutManager.getVgap
- def vGap_=(n: Int) { layoutManager.setVgap(n) }
+ def vGap_=(n: Int): Unit = layoutManager.setVgap(n)
def hGap: Int = layoutManager.getHgap
- def hGap_=(n: Int) { layoutManager.setHgap(n) }
+ def hGap_=(n: Int): Unit = layoutManager.setHgap(n)
}
--- a/src/Pure/General/completion.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/completion.scala Mon Mar 01 22:22:12 2021 +0100
@@ -103,7 +103,7 @@
frequency(item2.name) compare frequency(item1.name)
}
- def save()
+ def save(): Unit =
{
Isabelle_System.make_directory(COMPLETION_HISTORY.dir)
File.write_backup(COMPLETION_HISTORY,
@@ -119,7 +119,7 @@
private var history = History.empty
def value: History = synchronized { history }
- def load()
+ def load(): Unit =
{
val h = History.load()
synchronized { history = h }
--- a/src/Pure/General/csv.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/csv.scala Mon Mar 01 22:22:12 2021 +0100
@@ -28,6 +28,6 @@
override def toString: String = (Record(header:_*) :: records).mkString("\r\n")
def file_name: String = name + ".csv"
- def write(dir: Path) { isabelle.File.write(dir + Path.explode(file_name), toString) }
+ def write(dir: Path): Unit = isabelle.File.write(dir + Path.explode(file_name), toString)
}
}
--- a/src/Pure/General/exn.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/exn.scala Mon Mar 01 22:22:12 2021 +0100
@@ -102,9 +102,9 @@
def apply(): Throwable = new InterruptedException("Interrupt")
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
- def dispose() { Thread.interrupted }
- def expose() { if (Thread.interrupted) throw apply() }
- def impose() { 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 Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/file.scala Mon Mar 01 22:22:12 2021 +0100
@@ -160,7 +160,7 @@
follow_links: Boolean = false): List[JFile] =
{
val result = new mutable.ListBuffer[JFile]
- def check(file: JFile) { if (pred(file)) result += file }
+ def check(file: JFile): Unit = if (pred(file)) result += file
if (start.isFile) check(start)
else if (start.isDirectory) {
@@ -243,7 +243,8 @@
def writer(file: JFile): BufferedWriter =
new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
- def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
+ def write_file(
+ file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream): Unit =
{
val stream = make_stream(new FileOutputStream(file))
using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
@@ -263,13 +264,13 @@
write_xz(path.file, text, options)
def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
- def write_backup(path: Path, text: CharSequence)
+ def write_backup(path: Path, text: CharSequence): Unit =
{
if (path.is_file) Isabelle_System.move_file(path, path.backup)
write(path, text)
}
- def write_backup2(path: Path, text: CharSequence)
+ def write_backup2(path: Path, text: CharSequence): Unit =
{
if (path.is_file) Isabelle_System.move_file(path, path.backup2)
write(path, text)
@@ -318,7 +319,7 @@
else path.file.canExecute
}
- def set_executable(path: Path, flag: Boolean)
+ def set_executable(path: Path, flag: Boolean): Unit =
{
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
--- a/src/Pure/General/file_watcher.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/file_watcher.scala Mon Mar 01 22:22:12 2021 +0100
@@ -17,11 +17,11 @@
class File_Watcher private[File_Watcher] // dummy template
{
- def register(dir: JFile) { }
- def register_parent(file: JFile) { }
- def deregister(dir: JFile) { }
- def purge(retain: Set[JFile]) { }
- def shutdown() { }
+ def register(dir: JFile): Unit = {}
+ def register_parent(file: JFile): Unit = {}
+ def deregister(dir: JFile): Unit = {}
+ def purge(retain: Set[JFile]): Unit = {}
+ def shutdown(): Unit = {}
}
object File_Watcher
@@ -126,7 +126,7 @@
/* shutdown */
- override def shutdown()
+ override def shutdown(): Unit =
{
watcher_thread.interrupt
watcher_thread.join
--- a/src/Pure/General/graphics_file.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/graphics_file.scala Mon Mar 01 22:22:12 2021 +0100
@@ -22,7 +22,8 @@
{
/* PNG */
- def write_png(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72)
+ def write_png(
+ file: JFile, paint: Graphics2D => Unit, width: Int, height: Int, dpi: Int = 72): Unit =
{
val scale = dpi / 72.0f
val w = (width * scale).round
@@ -54,7 +55,7 @@
mapper
}
- def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
+ def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
{
import com.lowagie.text.{Document, Rectangle}
--- a/src/Pure/General/http.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/http.scala Mon Mar 01 22:22:12 2021 +0100
@@ -47,7 +47,7 @@
def read_request(): Bytes =
using(http_exchange.getRequestBody)(Bytes.read_stream(_))
- def write_response(code: Int, response: Response)
+ def write_response(code: Int, response: Response): Unit =
{
http_exchange.getResponseHeaders().set("Content-Type", response.content_type)
http_exchange.sendResponseHeaders(code, response.bytes.length.toLong)
@@ -64,7 +64,7 @@
}
def handler(root: String, body: Exchange => Unit): Handler =
- new Handler(root, new HttpHandler { def handle(x: HttpExchange) { body(new Exchange(x)) } })
+ new Handler(root, new HttpHandler { def handle(x: HttpExchange): Unit = body(new Exchange(x)) })
/* particular methods */
@@ -106,8 +106,8 @@
class Server private[HTTP](val http_server: HttpServer)
{
- def += (handler: Handler) { http_server.createContext(handler.root, handler.handler) }
- def -= (handler: Handler) { http_server.removeContext(handler.root) }
+ 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)
--- a/src/Pure/General/json.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/json.scala Mon Mar 01 22:22:12 2021 +0100
@@ -176,7 +176,7 @@
{
val result = new StringBuilder
- def string(s: String)
+ def string(s: String): Unit =
{
result += '"'
result ++=
@@ -195,7 +195,7 @@
result += '"'
}
- def array(list: List[T])
+ def array(list: List[T]): Unit =
{
result += '['
Library.separate(None, list.map(Some(_))).foreach({
@@ -205,7 +205,7 @@
result += ']'
}
- def object_(obj: Object.T)
+ def object_(obj: Object.T): Unit =
{
result += '{'
Library.separate(None, obj.toList.map(Some(_))).foreach({
@@ -218,7 +218,7 @@
result += '}'
}
- def json_format(x: T)
+ def json_format(x: T): Unit =
{
x match {
case null => result ++= "null"
--- a/src/Pure/General/linear_set.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/linear_set.scala Mon Mar 01 22:22:12 2021 +0100
@@ -24,7 +24,7 @@
private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]
{
private var res = empty[A]
- override def clear() { res = empty[A] }
+ override def clear(): Unit = { res = empty[A] }
override def addOne(elem: A): this.type = { res = res.incl(elem); this }
override def result(): Linear_Set[A] = res
}
--- a/src/Pure/General/logger.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/logger.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,12 +23,12 @@
object No_Logger extends Logger
{
- def apply(msg: => String) { }
+ def apply(msg: => String): Unit = {}
}
class File_Logger(path: Path) extends Logger
{
- def apply(msg: => String) { synchronized { File.append(path, msg + "\n") } }
+ def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
override def toString: String = path.toString
}
--- a/src/Pure/General/mercurial.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/mercurial.scala Mon Mar 01 22:22:12 2021 +0100
@@ -119,7 +119,8 @@
def parent(): String = log(rev = "p1()", template = "{node|short}")
- def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
+ def push(
+ remote: String = "", rev: String = "", force: Boolean = false, options: String = ""): Unit =
{
hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
check_rc(rc => rc == 0 | rc == 1)
@@ -129,7 +130,7 @@
hg.command("pull", opt_rev(rev) + optional(remote), options).check
def update(
- rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
+ rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = ""): Unit =
{
hg.command("update",
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
@@ -161,7 +162,7 @@
val outside = new mutable.ListBuffer[Path]
val unknown = new mutable.ListBuffer[Path]
- @tailrec def check(paths: List[Path])
+ @tailrec def check(paths: List[Path]): Unit =
{
paths match {
case path :: rest =>
@@ -185,7 +186,7 @@
/* setup remote vs. local repository */
- private def edit_hgrc(local_hg: Repository, path_name: String, source: String)
+ private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit =
{
val hgrc = local_hg.root + Path.explode(".hg/hgrc")
def header(line: String): Boolean = line.startsWith("[paths]")
@@ -230,7 +231,7 @@
remote_name: String = "",
path_name: String = default_path_name,
remote_exists: Boolean = false,
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
/* local repository */
--- a/src/Pure/General/multi_map.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/multi_map.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]
{
private var res = empty[A, B]
- override def clear() { res = empty[A, B] }
+ override def clear(): Unit = { res = empty[A, B] }
override def addOne(p: (A, B)): this.type = { res = res.insert(p._1, p._2); this }
override def result(): Multi_Map[A, B] = res
}
--- a/src/Pure/General/output.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/output.scala Mon Mar 01 22:22:12 2021 +0100
@@ -21,7 +21,7 @@
def error_prefix(s: String): String = Library.prefix_lines("*** ", s)
def error_message_text(msg: String): String = error_prefix(clean_yxml(msg))
- def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+ def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
{
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(writeln_text(msg) + "\n")
@@ -29,7 +29,7 @@
}
}
- def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+ def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
{
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(warning_text(msg) + "\n")
@@ -37,7 +37,7 @@
}
}
- def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
+ def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit =
{
if (msg.nonEmpty || include_empty) {
if (stdout) Console.print(error_message_text(msg) + "\n")
--- a/src/Pure/General/path.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/path.scala Mon Mar 01 22:22:12 2021 +0100
@@ -143,7 +143,7 @@
/* case-insensitive names */
- def check_case_insensitive(paths: List[Path])
+ def check_case_insensitive(paths: List[Path]): Unit =
{
val table =
(Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
--- a/src/Pure/General/scan.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/scan.scala Mon Mar 01 22:22:12 2021 +0100
@@ -478,7 +478,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 { buffered_stream.close }
+ def close: Unit = buffered_stream.close
}
new Paged_Reader(0)
}
--- a/src/Pure/General/sql.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/sql.scala Mon Mar 01 22:22:12 2021 +0100
@@ -196,8 +196,8 @@
object bool
{
- def update(i: Int, x: Boolean) { rep.setBoolean(i, x) }
- def update(i: Int, x: Option[Boolean])
+ def update(i: Int, x: Boolean): Unit = rep.setBoolean(i, x)
+ def update(i: Int, x: Option[Boolean]): Unit =
{
if (x.isDefined) update(i, x.get)
else rep.setNull(i, java.sql.Types.BOOLEAN)
@@ -205,8 +205,8 @@
}
object int
{
- def update(i: Int, x: Int) { rep.setInt(i, x) }
- def update(i: Int, x: Option[Int])
+ def update(i: Int, x: Int): Unit = rep.setInt(i, x)
+ def update(i: Int, x: Option[Int]): Unit =
{
if (x.isDefined) update(i, x.get)
else rep.setNull(i, java.sql.Types.INTEGER)
@@ -214,8 +214,8 @@
}
object long
{
- def update(i: Int, x: Long) { rep.setLong(i, x) }
- def update(i: Int, x: Option[Long])
+ def update(i: Int, x: Long): Unit = rep.setLong(i, x)
+ def update(i: Int, x: Option[Long]): Unit =
{
if (x.isDefined) update(i, x.get)
else rep.setNull(i, java.sql.Types.BIGINT)
@@ -223,8 +223,8 @@
}
object double
{
- def update(i: Int, x: Double) { rep.setDouble(i, x) }
- def update(i: Int, x: Option[Double])
+ def update(i: Int, x: Double): Unit = rep.setDouble(i, x)
+ def update(i: Int, x: Option[Double]): Unit =
{
if (x.isDefined) update(i, x.get)
else rep.setNull(i, java.sql.Types.DOUBLE)
@@ -232,12 +232,12 @@
}
object string
{
- def update(i: Int, x: String) { rep.setString(i, x) }
+ def update(i: Int, x: String): Unit = rep.setString(i, x)
def update(i: Int, x: Option[String]): Unit = update(i, x.orNull)
}
object bytes
{
- def update(i: Int, bytes: Bytes)
+ def update(i: Int, bytes: Bytes): Unit =
{
if (bytes == null) rep.setBytes(i, null)
else rep.setBinaryStream(i, bytes.stream(), bytes.length)
@@ -322,7 +322,7 @@
def connection: Connection
- def close() { connection.close }
+ def close(): Unit = connection.close
def transaction[A](body: => A): A =
{
@@ -432,7 +432,7 @@
def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
table.insert_cmd("INSERT OR IGNORE", sql = sql)
- def rebuild { using_statement("VACUUM")(_.execute()) }
+ def rebuild: Unit = using_statement("VACUUM")(_.execute())
}
}
@@ -509,6 +509,6 @@
table.insert_cmd("INSERT",
sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
- override def close() { super.close; port_forwarding.foreach(_.close) }
+ override def close(): Unit = { super.close; port_forwarding.foreach(_.close) }
}
}
--- a/src/Pure/General/ssh.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/ssh.scala Mon Mar 01 22:22:12 2021 +0100
@@ -157,7 +157,7 @@
/* logging */
- def logging(verbose: Boolean = true, debug: Boolean = false)
+ def logging(verbose: Boolean = true, debug: Boolean = false): Unit =
{
JSch.setLogger(if (verbose) new Logger(debug) else null)
}
@@ -166,7 +166,7 @@
{
def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug
- def log(level: Int, msg: String)
+ def log(level: Int, msg: String): Unit =
{
level match {
case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg)
@@ -213,7 +213,7 @@
override def toString: String =
local_host + ":" + local_port + ":" + remote_host + ":" + remote_port
- def close()
+ def close(): Unit =
{
ssh.session.delPortForwardingL(local_host, local_port)
if (ssh_close) ssh.close()
@@ -239,7 +239,7 @@
{
override def toString: String = "exec " + session.toString
- def close() { channel.disconnect }
+ def close(): Unit = channel.disconnect
val exit_status: Future[Int] =
Future.thread("ssh_wait") {
@@ -265,7 +265,7 @@
{
val result = new mutable.ListBuffer[String]
val line_buffer = new ByteArrayOutputStream(100)
- def line_flush()
+ def line_flush(): Unit =
{
val line = Library.trim_line(line_buffer.toString(UTF8.charset_name))
progress(line)
@@ -291,7 +291,7 @@
val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) }
val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) }
- def terminate()
+ def terminate(): Unit =
{
close
out_lines.join
@@ -347,7 +347,7 @@
val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
sftp.connect(connect_timeout(options))
- def close() { sftp.disconnect; session.disconnect; on_close() }
+ def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
val settings: Map[String, String] =
{
@@ -418,9 +418,9 @@
follow_links: Boolean = false): List[Path] =
{
val result = new mutable.ListBuffer[Path]
- def check(path: Path) { if (pred(path)) result += path }
+ def check(path: Path): Unit = { if (pred(path)) result += path }
- def find(dir: Path)
+ def find(dir: Path): Unit =
{
if (include_dirs) check(dir)
if (follow_links || !is_link(dir)) {
--- a/src/Pure/General/time.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/time.scala Mon Mar 01 22:22:12 2021 +0100
@@ -66,5 +66,5 @@
def instant: Instant = Instant.ofEpochMilli(ms)
- def sleep { Thread.sleep(ms) }
+ def sleep: Unit = Thread.sleep(ms)
}
--- a/src/Pure/General/utf8.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/utf8.scala Mon Mar 01 22:22:12 2021 +0100
@@ -32,7 +32,7 @@
val buf = new java.lang.StringBuilder(text.length)
var code = -1
var rest = 0
- def flush()
+ def flush(): Unit =
{
if (code != -1) {
if (rest == 0 && Character.isValidCodePoint(code))
@@ -42,13 +42,13 @@
rest = 0
}
}
- def init(x: Int, n: Int)
+ def init(x: Int, n: Int): Unit =
{
flush()
code = x
rest = n
}
- def push(x: Int)
+ def push(x: Int): Unit =
{
if (rest <= 0) init(x, -1)
else {
--- a/src/Pure/Isar/document_structure.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Isar/document_structure.scala Mon Mar 01 22:22:12 2021 +0100
@@ -69,7 +69,7 @@
var stack: List[(Command, mutable.ListBuffer[Document])] =
List((Command.empty, buffer()))
- def open(command: Command) { stack = (command, buffer()) :: stack }
+ def open(command: Command): Unit = { stack = (command, buffer()) :: stack }
def close(): Boolean =
stack match {
@@ -81,7 +81,7 @@
false
}
- def flush() { if (is_plain_theory(stack.head._1)) close() }
+ def flush(): Unit = if (is_plain_theory(stack.head._1)) close()
def result(): List[Document] =
{
@@ -89,7 +89,7 @@
stack.head._2.toList
}
- def add(command: Command)
+ def add(command: Command): Unit =
{
if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
else if (command.span.is_end) { flush(); close() }
@@ -125,7 +125,7 @@
private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
List((0, No_Item, buffer()))
- @tailrec private def close(level: Int => Boolean)
+ @tailrec private def close(level: Int => Boolean): Unit =
{
stack match {
case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
@@ -142,7 +142,7 @@
stack.head._3.toList
}
- def add(item: Item)
+ def add(item: Item): Unit =
{
item.heading_level match {
case Some(i) =>
--- a/src/Pure/Isar/outer_syntax.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Mon Mar 01 22:22:12 2021 +0100
@@ -166,7 +166,7 @@
val content = new mutable.ListBuffer[Token]
val ignored = new mutable.ListBuffer[Token]
- def ship(content: List[Token])
+ def ship(content: List[Token]): Unit =
{
val kind =
if (content.forall(_.is_ignored)) Command_Span.Ignored_Span
@@ -186,7 +186,7 @@
result += Command_Span.Span(kind, content)
}
- def flush()
+ def flush(): Unit =
{
if (content.nonEmpty) { ship(content.toList); content.clear }
if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
--- a/src/Pure/ML/ml_console.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/ML/ml_console.scala Mon Mar 01 22:22:12 2021 +0100
@@ -11,7 +11,7 @@
{
/* command line entry point */
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
var dirs: List[Path] = Nil
--- a/src/Pure/ML/ml_statistics.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Mon Mar 01 22:22:12 2021 +0100
@@ -54,9 +54,9 @@
def monitor(pid: Long,
stats_dir: String = "",
delay: Time = Time.seconds(0.5),
- consume: Properties.T => Unit = Console.println)
+ consume: Properties.T => Unit = Console.println): Unit =
{
- def progress_stdout(line: String)
+ def progress_stdout(line: String): Unit =
{
val props =
Library.space_explode(',', line).flatMap((entry: String) =>
@@ -289,7 +289,7 @@
/* charts */
- def update_data(data: XYSeriesCollection, selected_fields: List[String])
+ def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
data.removeAllSeries
for (field <- selected_fields) {
--- a/src/Pure/PIDE/byte_message.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/byte_message.scala Mon Mar 01 22:22:12 2021 +0100
@@ -60,7 +60,7 @@
private def make_header(ns: List[Int]): List[Bytes] =
List(Bytes(ns.mkString(",")), Bytes.newline)
- def write_message(stream: OutputStream, chunks: List[Bytes])
+ def write_message(stream: OutputStream, chunks: List[Bytes]): Unit =
{
write(stream, make_header(chunks.map(_.length)) ::: chunks)
flush(stream)
@@ -92,7 +92,7 @@
len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
}
- def write_line_message(stream: OutputStream, msg: Bytes)
+ def write_line_message(stream: OutputStream, msg: Bytes): Unit =
{
if (is_length(msg) || is_terminated(msg))
error ("Bad content for line message:\n" ++ msg.text.take(100))
--- a/src/Pure/PIDE/document.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/document.scala Mon Mar 01 22:22:12 2021 +0100
@@ -179,7 +179,7 @@
sealed abstract class Edit[A, B]
{
- def foreach(f: A => Unit)
+ def foreach(f: A => Unit): Unit =
{
this match {
case Edits(es) => es.foreach(f)
--- a/src/Pure/PIDE/editor.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/editor.scala Mon Mar 01 22:22:12 2021 +0100
@@ -27,8 +27,8 @@
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays
- def insert_overlay(command: Command, fn: String, args: List[String])
- def remove_overlay(command: Command, fn: String, args: List[String])
+ def insert_overlay(command: Command, fn: String, args: List[String]): Unit
+ def remove_overlay(command: Command, fn: String, args: List[String]): Unit
/* hyperlinks */
--- a/src/Pure/PIDE/headless.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/headless.scala Mon Mar 01 22:22:12 2021 +0100
@@ -278,7 +278,7 @@
Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit))
}
- def check_state(beyond_limit: Boolean = false)
+ def check_state(beyond_limit: Boolean = false): Unit =
{
val state = session.get_state()
for {
@@ -589,7 +589,7 @@
theories: List[Document.Node.Name],
files: List[Document.Node.Name],
unicode_symbols: Boolean,
- progress: Progress)
+ progress: Progress): Unit =
{
val loaded_theories =
for (node_name <- theories)
@@ -627,7 +627,7 @@
})
}
- def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
+ def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]): Unit =
{
state.change(st =>
{
@@ -637,7 +637,7 @@
})
}
- def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
+ def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]): Unit =
{
state.change(st =>
{
--- a/src/Pure/PIDE/protocol.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Mar 01 22:22:12 2021 +0100
@@ -300,7 +300,7 @@
/* protocol commands */
def protocol_command_raw(name: String, args: List[Bytes]): Unit
- def protocol_command_args(name: String, args: List[String])
+ def protocol_command_args(name: String, args: List[String]): Unit
def protocol_command(name: String, args: String*): Unit
@@ -352,7 +352,7 @@
blobs_yxml, toks_yxml, toks_sources)
}
- def define_command(resources: Resources, command: Command)
+ def define_command(resources: Resources, command: Command): Unit =
{
val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
encode_command(resources, command)
@@ -361,7 +361,7 @@
toks_yxml :: toks_sources)
}
- def define_commands(resources: Resources, commands: List[Command])
+ def define_commands(resources: Resources, commands: List[Command]): Unit =
{
protocol_command_args("Document.define_commands",
commands.map(command =>
@@ -376,7 +376,7 @@
}))
}
- def define_commands_bulk(resources: Resources, commands: List[Command])
+ def define_commands_bulk(resources: Resources, commands: List[Command]): Unit =
{
val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
irregular.foreach(define_command(resources, _))
@@ -400,7 +400,7 @@
/* document versions */
def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
- edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
+ edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]): Unit =
{
val consolidate_yxml =
{
@@ -433,7 +433,7 @@
Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
}
- def remove_versions(versions: List[Document.Version])
+ def remove_versions(versions: List[Document.Version]): Unit =
{
val versions_yxml =
{ import XML.Encode._
--- a/src/Pure/PIDE/prover.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/prover.scala Mon Mar 01 22:22:12 2021 +0100
@@ -70,24 +70,24 @@
{
/** receiver output **/
- private def system_output(text: String)
+ private def system_output(text: String): Unit =
{
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
- private def protocol_output(props: Properties.T, bytes: Bytes)
+ private def protocol_output(props: Properties.T, bytes: Bytes): Unit =
{
receiver(new Prover.Protocol_Output(cache.props(props), bytes))
}
- private def output(kind: String, props: Properties.T, body: XML.Body)
+ private def output(kind: String, props: Properties.T, body: XML.Body): Unit =
{
val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
val reports = Protocol_Message.reports(props, body)
for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg)))
}
- private def exit_message(result: Process_Result)
+ private def exit_message(result: Process_Result): Unit =
{
output(Markup.EXIT, Markup.Process_Result(result),
List(XML.Text(result.print_return_code)))
@@ -104,7 +104,7 @@
Process_Result(rc, timing = timing)
}
- private def terminate_process()
+ private def terminate_process(): Unit =
{
try { process.terminate }
catch {
@@ -161,9 +161,9 @@
/* management methods */
- def join() { process_manager.join() }
+ def join(): Unit = process_manager.join()
- def terminate()
+ def terminate(): Unit =
{
system_output("Terminating prover process")
command_input_close()
@@ -186,7 +186,7 @@
private def command_input_close(): Unit = command_input.foreach(_.shutdown)
- private def command_input_init(raw_stream: OutputStream)
+ private def command_input_init(raw_stream: OutputStream): Unit =
{
val name = "command_input"
val stream = new BufferedOutputStream(raw_stream)
@@ -357,7 +357,7 @@
case _ => error("Inactive prover input thread for command " + quote(name))
}
- def protocol_command_args(name: String, args: List[String])
+ def protocol_command_args(name: String, args: List[String]): Unit =
{
receiver(new Prover.Input(name, args))
protocol_command_raw(name, args.map(Bytes(_)))
--- a/src/Pure/PIDE/query_operation.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Mar 01 22:22:12 2021 +0100
@@ -54,7 +54,7 @@
def get_location: Option[Command] = current_state.value.location
- private def remove_overlay()
+ private def remove_overlay(): Unit =
{
val state = current_state.value
for (command <- state.location) {
@@ -65,7 +65,7 @@
/* content update */
- private def content_update()
+ private def content_update(): Unit =
{
editor.require_dispatcher {}
@@ -176,7 +176,7 @@
def cancel_query(): Unit =
editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
- def apply_query(query: List[String])
+ def apply_query(query: List[String]): Unit =
{
editor.require_dispatcher {}
@@ -200,7 +200,7 @@
}
}
- def locate_query()
+ def locate_query(): Unit =
{
editor.require_dispatcher {}
@@ -229,11 +229,13 @@
}
}
- def activate() {
+ def activate(): Unit =
+ {
editor.session.commands_changed += main
}
- def deactivate() {
+ def deactivate(): Unit =
+ {
editor.session.commands_changed -= main
remove_overlay()
current_state.change(_ => Query_Operation.State.empty)
--- a/src/Pure/PIDE/resources.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Mar 01 22:22:12 2021 +0100
@@ -278,7 +278,7 @@
consolidate: List[Document.Node.Name]): Session.Change =
Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
- def commit(change: Session.Change) { }
+ def commit(change: Session.Change): Unit = {}
/* theory and file dependencies */
--- a/src/Pure/PIDE/session.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/session.scala Mon Mar 01 22:22:12 2021 +0100
@@ -28,10 +28,10 @@
{
private val consumers = Synchronized[List[Consumer[A]]](Nil)
- def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
- def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
+ def += (c: Consumer[A]): Unit = consumers.change(Library.update(c))
+ def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c))
- def post(a: A)
+ def post(a: A): Unit =
{
for (c <- consumers.value.iterator) {
dispatcher.send(() =>
@@ -290,7 +290,7 @@
delay_flush.invoke()
}
- def shutdown()
+ def shutdown(): Unit =
{
delay_flush.revoke()
flush()
@@ -324,13 +324,13 @@
private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
private val state = Synchronized(init_state)
- def exit()
+ def exit(): Unit =
{
delay.revoke()
state.change(_ => None)
}
- def update(new_nodes: Set[Document.Node.Name] = Set.empty)
+ def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit =
{
val active =
state.change_result(st =>
@@ -351,9 +351,9 @@
def defined: Boolean = variable.value.isDefined
def get: Prover = variable.value.get
- def set(p: Prover) { variable.change(_ => Some(p)) }
- def reset { variable.change(_ => None) }
- def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
+ def set(p: Prover): Unit = variable.change(_ => Some(p))
+ def reset: Unit = variable.change(_ => None)
+ def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None })
}
@@ -401,7 +401,7 @@
def handle_raw_edits(
doc_blobs: Document.Blobs = Document.Blobs.empty,
edits: List[Document.Edit_Text] = Nil,
- consolidate: List[Document.Node.Name] = Nil)
+ consolidate: List[Document.Node.Name] = Nil): Unit =
//{{{
{
require(prover.defined, "prover process not defined (handle_raw_edits)")
@@ -420,7 +420,7 @@
/* resulting changes */
- def handle_change(change: Session.Change)
+ def handle_change(change: Session.Change): Unit =
//{{{
{
require(prover.defined, "prover process not defined (handle_change)")
@@ -428,7 +428,7 @@
// define commands
{
val id_commands = new mutable.ListBuffer[Command]
- def id_command(command: Command)
+ def id_command(command: Command): Unit =
{
for {
(name, digest) <- command.blobs_defined
@@ -467,16 +467,16 @@
/* prover output */
- def handle_output(output: Prover.Output)
+ def handle_output(output: Prover.Output): Unit =
//{{{
{
- def bad_output()
+ def bad_output(): Unit =
{
if (verbose)
Output.warning("Ignoring bad prover output: " + output.message.toString)
}
- def change_command(f: Document.State => (Command.State, Document.State))
+ def change_command(f: Document.State => (Command.State, Document.State)): Unit =
{
try {
val st = global_state.change_result(f)
@@ -721,7 +721,7 @@
else snapshot
}
- def start(start_prover: Prover.Receiver => Prover)
+ def start(start_prover: Prover.Receiver => Prover): Unit =
{
file_formats
_phase.change(
@@ -757,20 +757,18 @@
}
}
- def protocol_command(name: String, args: String*)
- { manager.send(Protocol_Command(name, args.toList)) }
+ def protocol_command(name: String, args: String*): Unit =
+ manager.send(Protocol_Command(name, args.toList))
- def cancel_exec(exec_id: Document_ID.Exec)
- { manager.send(Cancel_Exec(exec_id)) }
+ def cancel_exec(exec_id: Document_ID.Exec): Unit =
+ manager.send(Cancel_Exec(exec_id))
- def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
- {
+ def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit =
if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
- }
+
+ def update_options(options: Options): Unit =
+ manager.send_wait(Update_Options(options))
- def update_options(options: Options)
- { manager.send_wait(Update_Options(options)) }
-
- def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
- { manager.send(Session.Dialog_Result(id, serial, result)) }
+ def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit =
+ manager.send(Session.Dialog_Result(id, serial, result))
}
--- a/src/Pure/PIDE/text.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/text.scala Mon Mar 01 22:22:12 2021 +0100
@@ -92,7 +92,7 @@
{
val result = new mutable.ListBuffer[Range]
var last: Option[Range] = None
- def ship(next: Option[Range]) { result ++= last; last = next }
+ def ship(next: Option[Range]): Unit = { result ++= last; last = next }
for (range <- ranges.sortBy(_.start))
{
--- a/src/Pure/PIDE/xml.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Mar 01 22:22:12 2021 +0100
@@ -128,7 +128,7 @@
val header: String = "<?xml version=\"1.0\" encoding=\"utf-8\"?>\n"
- def output_char(s: StringBuilder, c: Char, permissive: Boolean = false)
+ def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit =
{
c match {
case '<' => s ++= "<"
@@ -140,13 +140,13 @@
}
}
- def output_string(s: StringBuilder, str: String, permissive: Boolean = false)
+ def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit =
{
if (str == null) s ++= str
else str.iterator.foreach(output_char(s, _, permissive = permissive))
}
- def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false)
+ def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit =
{
s += '<'
s ++= markup.name
@@ -162,7 +162,7 @@
s += '>'
}
- def output_elem_end(s: StringBuilder, name: String)
+ def output_elem_end(s: StringBuilder, name: String): Unit =
{
s += '<'
s += '/'
--- a/src/Pure/PIDE/yxml.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/yxml.scala Mon Mar 01 22:22:12 2021 +0100
@@ -32,7 +32,7 @@
/* string representation */
- def traversal(string: String => Unit, body: XML.Body)
+ def traversal(string: String => Unit, body: XML.Body): Unit =
{
def tree(t: XML.Tree): Unit =
t match {
@@ -83,26 +83,20 @@
def buffer(): mutable.ListBuffer[XML.Tree] = new mutable.ListBuffer[XML.Tree]
var stack: List[(Markup, mutable.ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
- def add(x: XML.Tree)
- {
+ def add(x: XML.Tree): Unit =
(stack: @unchecked) match { case (_, body) :: _ => body += x }
- }
- def push(name: String, atts: XML.Attributes)
- {
+ def push(name: String, atts: XML.Attributes): Unit =
if (name == "") err_element()
else stack = (cache.markup(Markup(name, atts)), buffer()) :: stack
- }
- def pop()
- {
+ def pop(): Unit =
(stack: @unchecked) match {
case (Markup.Empty, _) :: _ => err_unbalanced("")
case (markup, body) :: pending =>
stack = pending
add(cache.tree0(XML.Elem(markup, body.toList)))
}
- }
/* parse chunks */
--- a/src/Pure/System/bash.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/bash.scala Mon Mar 01 22:22:12 2021 +0100
@@ -128,7 +128,7 @@
// cleanup
- private def do_cleanup()
+ private def do_cleanup(): Unit =
{
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
--- a/src/Pure/System/command_line.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/command_line.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
var debug = false
- def tool(body: => Unit)
+ def tool(body: => Unit): Unit =
{
val thread =
Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
--- a/src/Pure/System/cygwin.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/cygwin.scala Mon Mar 01 22:22:12 2021 +0100
@@ -17,11 +17,11 @@
{
/* init (e.g. after extraction via 7zip) */
- def init(isabelle_root: String, cygwin_root: String)
+ def init(isabelle_root: String, cygwin_root: String): Unit =
{
require(Platform.is_windows, "Windows platform expected")
- def exec(cmdline: String*)
+ def exec(cmdline: String*): Unit =
{
val cwd = new JFile(isabelle_root)
val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
@@ -56,7 +56,7 @@
}
}
- def link(content: String, target: JFile)
+ def link(content: String, target: JFile): Unit =
{
val target_path = target.toPath
--- a/src/Pure/System/isabelle_fonts.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/isabelle_fonts.scala Mon Mar 01 22:22:12 2021 +0100
@@ -71,7 +71,7 @@
/* system init */
- def init()
+ def init(): Unit =
{
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
for (entry <- fonts()) ge.registerFont(entry.font)
--- a/src/Pure/System/isabelle_process.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala Mon Mar 01 22:22:12 2021 +0100
@@ -77,5 +77,5 @@
result
}
- def terminate { process.terminate }
+ def terminate: Unit = process.terminate
}
--- a/src/Pure/System/isabelle_system.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala Mon Mar 01 22:22:12 2021 +0100
@@ -80,7 +80,7 @@
if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
- def set_cygwin_root()
+ def set_cygwin_root(): Unit =
{
if (Platform.is_windows)
_settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
@@ -284,7 +284,7 @@
/* move files */
- def move_file(src: JFile, dst: JFile)
+ def move_file(src: JFile, dst: JFile): Unit =
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target))
@@ -296,7 +296,7 @@
/* symbolic link */
- def symlink(src: Path, dst: Path, force: Boolean = false)
+ def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
{
val src_file = src.file
val dst_file = dst.file
@@ -391,7 +391,7 @@
/* quasi-atomic update of directory */
- def update_directory(dir: Path, f: Path => Unit)
+ def update_directory(dir: Path, f: Path => Unit): Unit =
{
val new_dir = dir.ext("new")
val old_dir = dir.ext("old")
@@ -488,7 +488,7 @@
else error("Expected to find GNU tar executable")
}
- def require_command(cmds: String*)
+ def require_command(cmds: String*): Unit =
{
for (cmd <- cmds) {
if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd))
--- a/src/Pure/System/isabelle_tool.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/isabelle_tool.scala Mon Mar 01 22:22:12 2021 +0100
@@ -146,7 +146,7 @@
/* command line entry point */
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
args.toList match {
--- a/src/Pure/System/linux.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/linux.scala Mon Mar 01 22:22:12 2021 +0100
@@ -95,7 +95,7 @@
def user_add(name: String,
description: String = "",
system: Boolean = false,
- ssh_setup: Boolean = false)
+ ssh_setup: Boolean = false): Unit =
{
require(!description.contains(','), "malformed description")
@@ -124,19 +124,17 @@
def service_operation(op: String, name: String): Unit =
Isabelle_System.bash("systemctl " + Bash.string(op) + " " + Bash.string(name)).check
- def service_enable(name: String) { service_operation("enable", name) }
- def service_disable(name: String) { service_operation("disable", name) }
- def service_start(name: String) { service_operation("start", name) }
- def service_stop(name: String) { service_operation("stop", name) }
- def service_restart(name: String) { service_operation("restart", name) }
+ def service_enable(name: String): Unit = service_operation("enable", name)
+ def service_disable(name: String): Unit = service_operation("disable", name)
+ def service_start(name: String): Unit = service_operation("start", name)
+ def service_stop(name: String): Unit = service_operation("stop", name)
+ def service_restart(name: String): Unit = service_operation("restart", name)
- def service_shutdown(name: String)
- {
+ def service_shutdown(name: String): Unit =
try { service_stop(name) }
catch { case ERROR(_) => }
- }
- def service_install(name: String, spec: String)
+ def service_install(name: String, spec: String): Unit =
{
service_shutdown(name)
--- a/src/Pure/System/mingw.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/mingw.scala Mon Mar 01 22:22:12 2021 +0100
@@ -40,7 +40,7 @@
else if (root.isEmpty) error("Windows platform requires msys/mingw root specification")
else root.get
- def check
+ def check: Unit =
{
if (Platform.is_windows) {
get_root
--- a/src/Pure/System/options.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/options.scala Mon Mar 01 22:22:12 2021 +0100
@@ -390,7 +390,7 @@
/* save preferences */
- def save_prefs(file: Path = Options.PREFS)
+ def save_prefs(file: Path = Options.PREFS): Unit =
{
val defaults: Options = Options.init(prefs = "")
val changed =
--- a/src/Pure/System/posix_interrupt.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/posix_interrupt.scala Mon Mar 01 22:22:12 2021 +0100
@@ -15,7 +15,7 @@
def handler[A](h: => Unit)(e: => A): A =
{
val SIGINT = new Signal("INT")
- val new_handler = new SignalHandler { def handle(s: Signal) { h } }
+ val new_handler = new SignalHandler { def handle(s: Signal): Unit = h }
val old_handler = Signal.handle(SIGINT, new_handler)
try { e } finally { Signal.handle(SIGINT, old_handler) }
}
--- a/src/Pure/System/progress.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/progress.scala Mon Mar 01 22:22:12 2021 +0100
@@ -25,19 +25,19 @@
class Progress
{
- def echo(msg: String) {}
- def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
- def theory(theory: Progress.Theory) {}
- def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
+ def echo(msg: String): Unit = {}
+ def echo_if(cond: Boolean, msg: String): Unit = { if (cond) echo(msg) }
+ def theory(theory: Progress.Theory): Unit = {}
+ def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
- def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
- def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
+ def echo_warning(msg: String): Unit = echo(Output.warning_text(msg))
+ def echo_error_message(msg: String): Unit = echo(Output.error_message_text(msg))
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
Timing.timeit(message, enabled, echo)(e)
@volatile protected var is_stopped = false
- def stop { is_stopped = true }
+ def stop: Unit = { is_stopped = true }
def stopped: Boolean =
{
if (Thread.interrupted) is_stopped = true
@@ -45,7 +45,7 @@
}
def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
- def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
+ def expose_interrupt(): Unit = if (stopped) throw Exn.Interrupt()
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
def bash(script: String,
--- a/src/Pure/System/scala.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/scala.scala Mon Mar 01 22:22:12 2021 +0100
@@ -192,7 +192,7 @@
}
}
- private def cancel(id: String, future: Future[Unit])
+ private def cancel(id: String, future: Future[Unit]): Unit =
{
future.cancel
result(id, Scala.Tag.INTERRUPT, "")
@@ -202,7 +202,7 @@
{
msg.properties match {
case Markup.Invoke_Scala(name, id, thread) =>
- def body
+ def body: Unit =
{
val (tag, res) = Scala.function(name, msg.text)
result(id, tag, res)
--- a/src/Pure/System/system_channel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/system_channel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -25,7 +25,7 @@
override def toString: String = address
- def shutdown() { server.close }
+ def shutdown(): Unit = server.close
def rendezvous(): (OutputStream, InputStream) =
{
--- a/src/Pure/System/tty_loop.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/System/tty_loop.scala Mon Mar 01 22:22:12 2021 +0100
@@ -62,7 +62,7 @@
catch { case e: IOException => case Exn.Interrupt() => }
}
- def join { console_output.join; console_input.join }
+ def join: Unit = { console_output.join; console_input.join }
- def cancel { console_input.cancel }
+ def cancel: Unit = console_input.cancel
}
--- a/src/Pure/Thy/bibtex.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala Mon Mar 01 22:22:12 2021 +0100
@@ -87,7 +87,7 @@
def make_pos(length: Int): Position.T =
Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
- def advance_pos(tok: Token)
+ def advance_pos(tok: Token): Unit =
{
for (s <- Symbol.iterator(tok.source)) {
if (Symbol.is_newline(s)) line += 1
--- a/src/Pure/Thy/export.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/export.scala Mon Mar 01 22:22:12 2021 +0100
@@ -116,7 +116,7 @@
def uncompressed_yxml: XML.Body =
YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
- def write(db: SQL.Database)
+ def write(db: SQL.Database): Unit =
{
val (compressed, bytes) = body.join
db.using_statement(Data.table.insert())(stmt =>
@@ -339,7 +339,7 @@
progress: Progress = new Progress,
export_prune: Int = 0,
export_list: Boolean = false,
- export_patterns: List[String] = Nil)
+ export_patterns: List[String] = Nil): Unit =
{
using(store.open_database(session_name))(db =>
{
--- a/src/Pure/Thy/export_theory.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Mon Mar 01 22:22:12 2021 +0100
@@ -405,7 +405,7 @@
var seen = Set.empty[Long]
var result = SortedMap.empty[Long, (Thm_Id, Proof)]
- def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof)
+ def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof): Unit =
{
prf match {
case Term.Abst(_, _, p) => boxes(context, p)
--- a/src/Pure/Thy/file_format.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/file_format.scala Mon Mar 01 22:22:12 2021 +0100
@@ -41,13 +41,13 @@
def prover_options(options: Options): Options =
(options /: agents)({ case (opts, agent) => agent.prover_options(opts) })
- def stop_session { agents.foreach(_.stop) }
+ def stop_session: Unit = agents.foreach(_.stop)
}
trait Agent
{
def prover_options(options: Options): Options = options
- def stop {}
+ def stop: Unit = {}
}
object No_Agent extends Agent
--- a/src/Pure/Thy/html.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/html.scala Mon Mar 01 22:22:12 2021 +0100
@@ -142,7 +142,7 @@
}
def output(s: StringBuilder, text: String,
- control_blocks: Boolean, hidden: Boolean, permissive: Boolean)
+ control_blocks: Boolean, hidden: Boolean, permissive: Boolean): Unit =
{
def output_string(str: String): Unit =
XML.output_string(s, str, permissive = permissive)
@@ -208,7 +208,7 @@
Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
"ul", "ol", "dl", "li", "dt", "dd")
- def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean)
+ def output(s: StringBuilder, xml: XML.Body, hidden: Boolean, structural: Boolean): Unit =
{
def output_body(body: XML.Body): Unit =
{
@@ -401,7 +401,7 @@
def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
- def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
+ def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts")): Unit =
{
File.write(dir + isabelle_css.base,
fonts_css(make_url) + "\n\n" + File.read(isabelle_css))
@@ -413,7 +413,7 @@
def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
css: String = isabelle_css.file_name,
hidden: Boolean = true,
- structural: Boolean = true)
+ structural: Boolean = true): Unit =
{
init_dir(dir)
File.write(dir + Path.basic(name),
--- a/src/Pure/Thy/presentation.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
final class HTML_Context private[Presentation](fonts_url: String => String)
{
- def init_fonts(dir: Path)
+ def init_fonts(dir: Path): Unit =
{
val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
for (entry <- Isabelle_Fonts.fonts(hidden = true))
@@ -270,7 +270,7 @@
})
}
- def write_document(db: SQL.Database, session_name: String, doc: Document_Output)
+ def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
{
db.using_statement(Data.table.insert())(stmt =>
{
@@ -328,13 +328,14 @@
else Nil
}
- private def write_sessions(dir: Path, sessions: List[(String, String)])
+ private def write_sessions(dir: Path, sessions: List[(String, String)]): Unit =
{
import XML.Encode._
File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
}
- def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
+ def update_chapter_index(
+ browser_info: Path, chapter: String, new_sessions: List[(String, String)]): Unit =
{
val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
@@ -360,7 +361,7 @@
else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
}
- def make_global_index(browser_info: Path)
+ def make_global_index(browser_info: Path): Unit =
{
if (!(browser_info + Path.explode("index.html")).is_file) {
Isabelle_System.make_directory(browser_info)
@@ -403,7 +404,7 @@
verbose: Boolean = false,
html_context: HTML_Context,
elements: Elements,
- presentation: Context)
+ presentation: Context): Unit =
{
val info = deps.sessions_structure(session)
val options = info.options
--- a/src/Pure/Thy/sessions.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Mar 01 22:22:12 2021 +0100
@@ -753,7 +753,7 @@
def theory_qualifier(name: String): String =
global_theories.getOrElse(name, Long_Name.qualifier(name))
- def check_sessions(names: List[String])
+ def check_sessions(names: List[String]): Unit =
{
val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
if (bad_sessions.nonEmpty)
@@ -1210,7 +1210,7 @@
{
def cache: XML.Cache = store.cache
- def close { 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 {
@@ -1304,7 +1304,7 @@
def output_log(name: String): Path = output_dir + log(name)
def output_log_gz(name: String): Path = output_dir + log_gz(name)
- def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) }
+ def prepare_output_dir(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
/* heap */
@@ -1411,7 +1411,7 @@
/* session info */
- def init_session_info(db: SQL.Database, name: String)
+ def init_session_info(db: SQL.Database, name: String): Unit =
{
db.transaction {
db.create_table(Session_Info.table)
@@ -1450,7 +1450,7 @@
db: SQL.Database,
name: String,
build_log: Build_Log.Session_Info,
- build: Build.Session_Info)
+ build: Build.Session_Info): Unit =
{
db.transaction {
db.using_statement(Session_Info.table.insert())(stmt =>
--- a/src/Pure/Thy/thy_syntax.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Mon Mar 01 22:22:12 2021 +0100
@@ -27,7 +27,7 @@
val visible = new mutable.ListBuffer[Command]
val visible_overlay = new mutable.ListBuffer[Command]
@tailrec
- def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
+ def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)]): Unit =
{
(ranges, commands) match {
case (range :: more_ranges, (command, offset) #:: more_commands) =>
--- a/src/Pure/Tools/build.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/build.scala Mon Mar 01 22:22:12 2021 +0100
@@ -302,10 +302,8 @@
}
}
- def sleep()
- {
+ def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
- }
val numa_nodes = new NUMA.Nodes(numa_shuffling)
--- a/src/Pure/Tools/build_docker.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/build_docker.scala Mon Mar 01 22:22:12 2021 +0100
@@ -31,7 +31,7 @@
output: Option[Path] = None,
more_packages: List[String] = Nil,
tag: String = "",
- verbose: Boolean = false)
+ verbose: Boolean = false): Unit =
{
val isabelle_name =
app_archive match {
--- a/src/Pure/Tools/build_job.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Mar 01 22:22:12 2021 +0100
@@ -90,7 +90,7 @@
margin: Double = Pretty.default_margin,
breakgain: Double = Pretty.default_breakgain,
metric: Pretty.Metric = Symbol.Metric,
- unicode_symbols: Boolean = false)
+ unicode_symbols: Boolean = false): Unit =
{
val store = Sessions.store(options)
@@ -254,7 +254,7 @@
def result: Exn.Result[List[String]] = promise.join_result
def cancel: Unit = promise.cancel
- def apply(errs: List[String])
+ def apply(errs: List[String]): Unit =
{
try { promise.fulfill(errs) }
catch { case _: IllegalStateException => }
@@ -286,7 +286,7 @@
session.init_protocol_handler(new Session.Protocol_Handler
{
- override def exit() { Build_Session_Errors.cancel }
+ override def exit(): Unit = Build_Session_Errors.cancel
private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
{
@@ -357,7 +357,7 @@
case snapshot =>
val rendering = new Rendering(snapshot, options, session)
- def export(name: String, xml: XML.Body, compress: Boolean = true)
+ def export(name: String, xml: XML.Body, compress: Boolean = true): Unit =
{
val theory_name = snapshot.node_name.theory
val args =
--- a/src/Pure/Tools/check_keywords.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/check_keywords.scala Mon Mar 01 22:22:12 2021 +0100
@@ -35,7 +35,7 @@
progress: Progress,
keywords: Keyword.Keywords,
check: Set[String],
- paths: List[Path])
+ paths: List[Path]): Unit =
{
val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
--- a/src/Pure/Tools/debugger.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/debugger.scala Mon Mar 01 22:22:12 2021 +0100
@@ -162,13 +162,13 @@
/* protocol commands */
- def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State])
+ def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]): Unit =
{
state.change(_.update_thread(thread_name, debug_states))
delay_update.invoke()
}
- def add_output(thread_name: String, entry: Command.Results.Entry)
+ def add_output(thread_name: String, entry: Command.Results.Entry): Unit =
{
state.change(_.add_output(thread_name, entry))
delay_update.invoke()
@@ -176,7 +176,7 @@
def is_active(): Boolean = session.is_ready && state.value.is_active
- def ready()
+ def ready(): Unit =
{
if (is_active())
session.protocol_command("Debugger.init")
@@ -201,7 +201,7 @@
})
def is_break(): Boolean = state.value.break
- def set_break(b: Boolean)
+ def set_break(b: Boolean): Unit =
{
state.change(st => {
val st1 = st.set_break(b)
@@ -220,7 +220,7 @@
def breakpoint_state(breakpoint: Long): Boolean =
state.value.active_breakpoints(breakpoint)
- def toggle_breakpoint(command: Command, breakpoint: Long)
+ def toggle_breakpoint(command: Command, breakpoint: Long): Unit =
{
state.change(st =>
{
@@ -252,7 +252,7 @@
}
def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
- def set_focus(c: Debugger.Context)
+ def set_focus(c: Debugger.Context): Unit =
{
state.change(_.set_focus(c))
delay_update.invoke()
@@ -266,13 +266,13 @@
def step_over(thread_name: String): Unit = input(thread_name, "step_over")
def step_out(thread_name: String): Unit = input(thread_name, "step_out")
- def clear_output(thread_name: String)
+ def clear_output(thread_name: String): Unit =
{
state.change(_.clear_output(thread_name))
delay_update.invoke()
}
- def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
+ def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String): Unit =
{
state.change(st => {
input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
@@ -282,7 +282,7 @@
delay_update.invoke()
}
- def print_vals(c: Debugger.Context, SML: Boolean, context: String)
+ def print_vals(c: Debugger.Context, SML: Boolean, context: String): Unit =
{
require(c.debug_index.isDefined)
--- a/src/Pure/Tools/doc.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/doc.scala Mon Mar 01 22:22:12 2021 +0100
@@ -84,7 +84,7 @@
/* view */
- def view(path: Path)
+ def view(path: Path): Unit =
{
if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
else {
--- a/src/Pure/Tools/dump.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/dump.scala Mon Mar 01 22:22:12 2021 +0100
@@ -138,7 +138,7 @@
def session_dirs: List[Path] = dirs ::: select_dirs
- def build_logic(logic: String)
+ def build_logic(logic: String): Unit =
{
Build.build_logic(options, logic, build_heap = true, progress = progress,
dirs = session_dirs, strict = true)
@@ -226,12 +226,12 @@
private val errors = Synchronized(List.empty[String])
- def add_errors(more_errs: List[String])
+ def add_errors(more_errs: List[String]): Unit =
{
errors.change(errs => errs ::: more_errs)
}
- def check_errors
+ def check_errors: Unit =
{
val errs = errors.value
if (errs.nonEmpty) error(errs.mkString("\n\n"))
@@ -289,7 +289,7 @@
/* process */
- def process(process_theory: Args => Unit, unicode_symbols: Boolean = false)
+ def process(process_theory: Args => Unit, unicode_symbols: Boolean = false): Unit =
{
val session = resources.start_session(progress = progress)
@@ -394,7 +394,7 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
output_dir: Path = default_output_dir,
- selection: Sessions.Selection = Sessions.Selection.empty)
+ selection: Sessions.Selection = Sessions.Selection.empty): Unit =
{
val context =
Context(options, aspects = aspects, progress = progress, dirs = dirs,
--- a/src/Pure/Tools/java_monitor.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/java_monitor.scala Mon Mar 01 22:22:12 2021 +0100
@@ -26,7 +26,7 @@
def java_monitor_internal(
pid: Long = default_pid,
look_and_feel: String = "",
- update_interval: Time = default_update_interval)
+ update_interval: Time = default_update_interval): Unit =
{
val vm =
if (pid.toInt.toLong == pid) LocalVirtualMachine.getLocalVirtualMachine(pid.toInt)
@@ -102,7 +102,7 @@
parent: Component,
pid: Long = default_pid,
look_and_feel: String = "",
- update_interval: Time = default_update_interval)
+ update_interval: Time = default_update_interval): Unit =
{
Future.thread(name = "java_monitor", daemon = true) {
try {
@@ -124,7 +124,7 @@
/* command line entry point */
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
Command_Line.tool {
var look_and_feel = ""
--- a/src/Pure/Tools/main.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/main.scala Mon Mar 01 22:22:12 2021 +0100
@@ -14,7 +14,7 @@
{
/* main entry point */
- def main(args: Array[String])
+ def main(args: Array[String]): Unit =
{
if (args.nonEmpty && args(0) == "-init") {
Isabelle_System.init()
@@ -108,7 +108,7 @@
/* environment */
- def putenv(name: String, value: String)
+ def putenv(name: String, value: String): Unit =
{
val misc =
Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
--- a/src/Pure/Tools/mkroot.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/mkroot.scala Mon Mar 01 22:22:12 2021 +0100
@@ -25,7 +25,7 @@
init_repos: Boolean = false,
title: String = "",
author: String = "",
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
Isabelle_System.make_directory(session_dir)
--- a/src/Pure/Tools/phabricator.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/phabricator.scala Mon Mar 01 22:22:12 2021 +0100
@@ -129,7 +129,7 @@
else Nil
}
- def write_config(configs: List[Config])
+ def write_config(configs: List[Config]): Unit =
{
File.write(global_config,
configs.map(config => config.name + ":" + config.root.implode).mkString("", "\n", "\n"))
@@ -187,7 +187,7 @@
/** setup **/
- def user_setup(name: String, description: String, ssh_setup: Boolean = false)
+ def user_setup(name: String, description: String, ssh_setup: Boolean = false): Unit =
{
if (!Linux.user_exists(name)) {
Linux.user_add(name, description = description, system = true, ssh_setup = ssh_setup)
@@ -210,7 +210,7 @@
command
}
- def mercurial_setup(mercurial_source: String, progress: Progress = new Progress)
+ def mercurial_setup(mercurial_source: String, progress: Progress = new Progress): Unit =
{
progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
Isabelle_System.with_tmp_dir("mercurial")(tmp_dir =>
@@ -237,7 +237,7 @@
repo: String = "",
package_update: Boolean = false,
mercurial_source: String = "",
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
/* system environment */
@@ -604,7 +604,7 @@
name: String = default_name,
config_file: Option[Path] = None,
test_user: String = "",
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
Linux.check_system_root()
@@ -613,7 +613,7 @@
val mail_config = config_file getOrElse default_config_file
- def setup_mail
+ def setup_mail: Unit =
{
progress.echo("Using mail configuration from " + mail_config)
config.execute("config set cluster.mailers --stdin < " + File.bash_path(mail_config))
@@ -722,7 +722,7 @@
def phabricator_setup_ssh(
server_port: Int = default_server_port,
system_port: Int = default_system_port,
- progress: Progress = new Progress)
+ progress: Progress = new Progress): Unit =
{
Linux.check_system_root()
--- a/src/Pure/Tools/scala_project.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala Mon Mar 01 22:22:12 2021 +0100
@@ -104,7 +104,7 @@
/* scala project */
- def scala_project(project_dir: Path, symlinks: Boolean = false)
+ def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
{
if (symlinks && Platform.is_windows)
error("Cannot create symlinks on Windows")
--- a/src/Pure/Tools/server.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/server.scala Mon Mar 01 22:22:12 2021 +0100
@@ -148,9 +148,9 @@
}
}
- def start { thread }
- def join { thread.join }
- def stop { socket.close; join }
+ def start: Unit = thread
+ def join: Unit = thread.join
+ def stop: Unit = { socket.close; join }
}
@@ -166,9 +166,9 @@
{
override def toString: String = socket.toString
- def close() { socket.close }
+ def close(): Unit = socket.close
- def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
+ def set_timeout(t: Time): Unit = socket.setSoTimeout(t.ms.toInt)
private val in = new BufferedInputStream(socket.getInputStream)
private val out = new BufferedOutputStream(socket.getOutputStream)
@@ -195,18 +195,18 @@
def write_message(msg: String): Unit =
out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) }
- def reply(r: Reply.Value, arg: Any)
+ def reply(r: Reply.Value, arg: Any): Unit =
{
val argument = Argument.print(arg)
write_message(if (argument == "") r.toString else r.toString + " " + argument)
}
- def reply_ok(arg: Any) { reply(Reply.OK, arg) }
- def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
+ def reply_ok(arg: Any): Unit = reply(Reply.OK, arg)
+ def reply_error(arg: Any): Unit = reply(Reply.ERROR, arg)
def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
reply_error(Reply.error_message(message) ++ more)
- def notify(arg: Any) { reply(Reply.NOTE, arg) }
+ def notify(arg: Any): Unit = reply(Reply.NOTE, arg)
}
@@ -219,8 +219,8 @@
def command_list: List[String] = command_table.keys.toList.sorted
- def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
- def notify(arg: Any) { connection.notify(arg) }
+ def reply(r: Reply.Value, arg: Any): Unit = connection.reply(r, arg)
+ def notify(arg: Any): Unit = connection.notify(arg)
def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
notify(Reply.message(msg, kind = kind) ++ more)
def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
@@ -251,7 +251,7 @@
def cancel_task(id: UUID.T): Unit =
_tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
- def close()
+ def close(): Unit =
{
while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
{ _tasks.value.foreach(_.join) }
@@ -265,7 +265,7 @@
override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
- override def theory(theory: Progress.Theory)
+ override def theory(theory: Progress.Theory): Unit =
{
val entries: List[JSON.Object.Entry] =
List("theory" -> theory.theory, "session" -> theory.session) :::
@@ -273,7 +273,7 @@
context.writeln(theory.message, entries ::: more.toList:_*)
}
- override def nodes_status(nodes_status: Document_Status.Nodes_Status)
+ override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
{
val json =
for ((name, node_status) <- nodes_status.present)
@@ -292,7 +292,7 @@
val ident: JSON.Object.Entry = ("task" -> id.toString)
val progress: Connection_Progress = context.progress(ident)
- def cancel { progress.stop }
+ def cancel: Unit = progress.stop
private lazy val thread = Isabelle_Thread.fork(name = "server_task")
{
@@ -306,8 +306,8 @@
progress.stop
context.remove_task(task)
}
- def start { thread }
- def join { thread.join }
+ def start: Unit = thread
+ def join: Unit = thread.join
}
@@ -521,7 +521,7 @@
private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
- def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
+ def add_session(entry: (UUID.T, Headless.Session)): Unit = _sessions.change(_ + entry)
def remove_session(id: UUID.T): Headless.Session =
{
_sessions.change_result(sessions =>
@@ -531,7 +531,7 @@
})
}
- def shutdown()
+ def shutdown(): Unit =
{
server.socket.close
@@ -545,9 +545,9 @@
}
}
- override def join { super.join; shutdown() }
+ override def join: Unit = { super.join; shutdown() }
- override def handle(connection: Server.Connection)
+ override def handle(connection: Server.Connection): Unit =
{
using(new Server.Context(server, connection))(context =>
{
--- a/src/Pure/Tools/simplifier_trace.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Mon Mar 01 22:22:12 2021 +0100
@@ -153,7 +153,7 @@
(id, context.questions(serial))
}
- def do_cancel(serial: Long, id: Document_ID.Command)
+ def do_cancel(serial: Long, id: Document_ID.Command): Unit =
{
// To save memory, we could try to remove empty contexts at this point.
// However, if a new serial gets attached to the same command_id after we deleted
@@ -162,7 +162,7 @@
contexts += (id -> (contexts(id) - serial))
}
- def do_reply(session: Session, serial: Long, answer: Answer)
+ def do_reply(session: Session, serial: Long, answer: Answer): Unit =
{
session.protocol_command(
"Simplifier_Trace.reply", Value.Long(serial), answer.name)
@@ -298,14 +298,14 @@
{
private var the_session: Session = null
- override def init(session: Session)
+ override def init(session: Session): Unit =
{
try { the_manager(session) }
catch { case ERROR(_) => managers.change(map => map + (session -> make_manager)) }
the_session = session
}
- override def exit()
+ override def exit(): Unit =
{
val session = the_session
if (session != null) {
--- a/src/Pure/Tools/spell_checker.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/spell_checker.scala Mon Mar 01 22:22:12 2021 +0100
@@ -28,7 +28,7 @@
def apostrophe(c: Int): Boolean =
c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
- @tailrec def scan(pred: Int => Boolean)
+ @tailrec def scan(pred: Int => Boolean): Unit =
{
if (offset < text.length) {
val c = text.codePointAt(offset)
@@ -125,7 +125,7 @@
case None => false
}
- private def load()
+ private def load(): Unit =
{
val main_dictionary = split_lines(File.read_gzip(dictionary.path))
@@ -154,7 +154,7 @@
}
load()
- private def save()
+ private def save(): Unit =
{
val permanent_decls =
(for {
@@ -178,7 +178,7 @@
}
}
- def update(word: String, include: Boolean, permanent: Boolean)
+ def update(word: String, include: Boolean, permanent: Boolean): Unit =
{
updates += (word -> Spell_Checker.Update(include, permanent))
@@ -189,7 +189,7 @@
else { save(); load() }
}
- def reset()
+ def reset(): Unit =
{
updates = SortedMap.empty
load()
--- a/src/Pure/Tools/update.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update.scala Mon Mar 01 22:22:12 2021 +0100
@@ -14,7 +14,7 @@
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
- selection: Sessions.Selection = Sessions.Selection.empty)
+ selection: Sessions.Selection = Sessions.Selection.empty): Unit =
{
val context =
Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
--- a/src/Pure/Tools/update_cartouches.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update_cartouches.scala Mon Mar 01 22:22:12 2021 +0100
@@ -37,7 +37,7 @@
}
}
- def update_cartouches(replace_text: Boolean, path: Path)
+ def update_cartouches(replace_text: Boolean, path: Path): Unit =
{
val text0 = File.read(path)
--- a/src/Pure/Tools/update_comments.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update_comments.scala Mon Mar 01 22:22:12 2021 +0100
@@ -12,7 +12,7 @@
object Update_Comments
{
- def update_comments(path: Path)
+ def update_comments(path: Path): Unit =
{
def make_comment(tok: Token): String =
Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content))
--- a/src/Pure/Tools/update_header.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update_header.scala Mon Mar 01 22:22:12 2021 +0100
@@ -9,7 +9,7 @@
object Update_Header
{
- def update_header(section: String, path: Path)
+ def update_header(section: String, path: Path): Unit =
{
val text0 = File.read(path)
val text1 =
--- a/src/Pure/Tools/update_then.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update_then.scala Mon Mar 01 22:22:12 2021 +0100
@@ -9,7 +9,7 @@
object Update_Then
{
- def update_then(path: Path)
+ def update_then(path: Path): Unit =
{
val text0 = File.read(path)
val text1 =
--- a/src/Pure/Tools/update_theorems.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Tools/update_theorems.scala Mon Mar 01 22:22:12 2021 +0100
@@ -9,7 +9,7 @@
object Update_Theorems
{
- def update_theorems(path: Path)
+ def update_theorems(path: Path): Unit =
{
val text0 = File.read(path)
val text1 =
--- a/src/Tools/Graphview/graph_file.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/graph_file.scala Mon Mar 01 22:22:12 2021 +0100
@@ -15,13 +15,13 @@
object Graph_File
{
- def write(file: JFile, graphview: Graphview)
+ def write(file: JFile, graphview: Graphview): Unit =
{
val box = graphview.bounding_box()
val w = box.width.ceil.toInt
val h = box.height.ceil.toInt
- def paint(gfx: Graphics2D)
+ def paint(gfx: Graphics2D): Unit =
{
gfx.setColor(graphview.background_color)
gfx.fillRect(0, 0, w, h)
@@ -35,7 +35,7 @@
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
}
- def write(options: Options, file: JFile, graph: Graph_Display.Graph)
+ def write(options: Options, file: JFile, graph: Graph_Display.Graph): Unit =
{
val the_options = options
val graphview =
--- a/src/Tools/Graphview/graph_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -32,7 +32,7 @@
private val painter = new Panel
{
- override def paint(gfx: Graphics2D)
+ override def paint(gfx: Graphics2D): Unit =
{
super.paintComponent(gfx)
@@ -44,7 +44,7 @@
}
}
- def set_preferred_size()
+ def set_preferred_size(): Unit =
{
val box = graphview.bounding_box()
val s = Transform.scale_discrete
@@ -52,7 +52,7 @@
painter.revalidate()
}
- def refresh()
+ def refresh(): Unit =
{
if (painter != null) {
set_preferred_size()
@@ -60,7 +60,7 @@
}
}
- def scroll_to_node(node: Graph_Display.Node)
+ def scroll_to_node(node: Graph_Display.Node): Unit =
{
val gap = graphview.metrics.gap
val info = graphview.layout.get_node(node)
@@ -120,14 +120,14 @@
/* transform */
- def rescale(s: Double)
+ def rescale(s: Double): Unit =
{
Transform.scale = s
if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
refresh()
}
- def fit_to_window()
+ def fit_to_window(): Unit =
{
Transform.fit_to_window()
refresh()
@@ -137,7 +137,7 @@
{
private var _scale: Double = 1.0
def scale: Double = _scale
- def scale_=(s: Double)
+ def scale_=(s: Double): Unit =
{
_scale = (s min 10.0) max 0.1
}
@@ -156,7 +156,7 @@
t
}
- def fit_to_window()
+ def fit_to_window(): Unit =
{
if (graphview.visible_graph.is_empty)
rescale(1.0)
@@ -187,7 +187,7 @@
private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =
(new Point(0, 0), Nil, Nil)
- def pressed(at: Point)
+ def pressed(at: Point): Unit =
{
val c = Transform.pane_to_graph_coordinates(at)
val l =
@@ -205,7 +205,7 @@
draginfo = (at, l, d)
}
- def dragged(to: Point)
+ def dragged(to: Point): Unit =
{
val (from, p, d) = draginfo
@@ -229,7 +229,7 @@
draginfo = (to, p, d)
}
- def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean)
+ def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean): Unit =
{
val c = Transform.pane_to_graph_coordinates(at)
--- a/src/Tools/Graphview/graphview.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/graphview.scala Mon Mar 01 22:22:12 2021 +0100
@@ -67,7 +67,7 @@
new Rectangle2D.Double(x0, y0, x1 - x0, y1 - y0)
}
- def update_layout()
+ def update_layout(): Unit =
{
val metrics = Metrics(make_font())
val visible_graph = model.make_visible_graph()
@@ -139,7 +139,7 @@
}
}
- def paint(gfx: Graphics2D)
+ def paint(gfx: Graphics2D): Unit =
{
gfx.setRenderingHints(Metrics.rendering_hints)
--- a/src/Tools/Graphview/main_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/main_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
leftComponent = tree_panel
rightComponent = graph_panel
- def update_layout()
+ def update_layout(): Unit =
{
graphview.update_layout()
tree_panel.refresh()
--- a/src/Tools/Graphview/model.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/model.scala Mon Mar 01 22:22:12 2021 +0100
@@ -19,13 +19,13 @@
private var _mutators : List[Mutator.Info] = Nil
def apply(): List[Mutator.Info] = _mutators
- def apply(mutators: List[Mutator.Info])
+ def apply(mutators: List[Mutator.Info]): Unit =
{
_mutators = mutators
events.event(Mutator_Event.New_List(mutators))
}
- def add(mutator: Mutator.Info)
+ def add(mutator: Mutator.Info): Unit =
{
_mutators = _mutators ::: List(mutator)
events.event(Mutator_Event.Add(mutator))
@@ -61,7 +61,7 @@
private var _colors = Map.empty[Graph_Display.Node, Color]
def colors = _colors
- private def build_colors()
+ private def build_colors(): Unit =
{
_colors =
(Map.empty[Graph_Display.Node, Color] /: Colors()) {
--- a/src/Tools/Graphview/mutator_dialog.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Mon Mar 01 22:22:12 2021 +0100
@@ -31,7 +31,7 @@
private var _panels: List[Mutator_Panel] = Nil
private def panels = _panels
- private def panels_=(panels: List[Mutator_Panel])
+ private def panels_=(panels: List[Mutator_Panel]): Unit =
{
_panels = panels
paint_panels()
@@ -43,7 +43,7 @@
case Mutator_Event.New_List(ms) => panels = get_panels(ms)
}
- override def open()
+ override def open(): Unit =
{
if (!visible) panels = get_panels(container())
super.open
@@ -82,17 +82,17 @@
panels = moveDown(panels)
}
- private def removePanel(m: Mutator_Panel)
+ private def removePanel(m: Mutator_Panel): Unit =
{
panels = panels.filter(_ != m).toList
}
- private def add_panel(m: Mutator_Panel)
+ private def add_panel(m: Mutator_Panel): Unit =
{
panels = panels ::: List(m)
}
- def paint_panels()
+ def paint_panels(): Unit =
{
Focus_Traveral_Policy.clear
filter_panel.contents.clear
@@ -351,9 +351,9 @@
{
private var items = Vector.empty[java.awt.Component]
- def add(c: java.awt.Component) { items = items :+ c }
- def addAll(cs: TraversableOnce[java.awt.Component]) { items = items ++ cs }
- def clear() { items = Vector.empty }
+ def add(c: java.awt.Component): Unit = { items = items :+ c }
+ def addAll(cs: TraversableOnce[java.awt.Component]): Unit = { items = items ++ cs }
+ def clear(): Unit = { items = Vector.empty }
def getComponentAfter(root: java.awt.Container, c: java.awt.Component): java.awt.Component =
{
--- a/src/Tools/Graphview/mutator_event.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/mutator_event.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,8 +23,8 @@
{
private val receivers = Synchronized[List[Receiver]](Nil)
- def += (r: Receiver) { receivers.change(Library.insert(r)) }
- def -= (r: Receiver) { receivers.change(Library.remove(r)) }
- def event(x: Message) { receivers.value.reverse.foreach(r => r(x)) }
+ def += (r: Receiver): Unit = receivers.change(Library.insert(r))
+ def -= (r: Receiver): Unit = receivers.change(Library.remove(r))
+ def event(x: Message): Unit = receivers.value.reverse.foreach(r => r(x))
}
}
\ No newline at end of file
--- a/src/Tools/Graphview/shapes.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/shapes.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
def shape(info: Layout.Info): Rectangle2D.Double =
new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height)
- def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
+ def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit =
{
val metrics = graphview.metrics
val extra = metrics.char_width
@@ -37,7 +37,7 @@
info.height + 2 * extra))
}
- def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node)
+ def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit =
{
val metrics = graphview.metrics
val info = graphview.layout.get_node(node)
@@ -66,7 +66,7 @@
}
}
- def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info)
+ def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info): Unit =
{
gfx.setStroke(default_stroke)
gfx.setColor(graphview.dummy_color)
@@ -75,7 +75,7 @@
object Straight_Edge
{
- def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
+ def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit =
{
val p = graphview.layout.get_node(edge._1)
val q = graphview.layout.get_node(edge._2)
@@ -105,7 +105,7 @@
{
private val slack = 0.1
- def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge)
+ def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit =
{
val p = graphview.layout.get_node(edge._1)
val q = graphview.layout.get_node(edge._2)
@@ -210,7 +210,7 @@
}
}
- def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape)
+ def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape): Unit =
{
position(path, shape) match {
case None =>
--- a/src/Tools/Graphview/tree_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,7 @@
{
/* main actions */
- private def selection_action()
+ private def selection_action(): Unit =
{
if (tree != null) {
graphview.current_node = None
@@ -45,7 +45,7 @@
}
}
- private def point_action(path: TreePath)
+ private def point_action(path: TreePath): Unit =
{
if (tree_pane != null && path != null) {
val action_node =
@@ -131,11 +131,12 @@
if (ok) selection_field_foreground else graphview.error_color
}
- selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
- def changedUpdate(e: DocumentEvent) { selection_delay.invoke() }
- def insertUpdate(e: DocumentEvent) { selection_delay.invoke() }
- def removeUpdate(e: DocumentEvent) { selection_delay.invoke() }
- })
+ selection_field.peer.getDocument.addDocumentListener(
+ new DocumentListener {
+ def changedUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ def insertUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ def removeUpdate(e: DocumentEvent): Unit = selection_delay.invoke()
+ })
private val selection_apply = new Button {
action = Action("<html><b>Apply</b></html>") { selection_action () }
@@ -148,7 +149,7 @@
/* main layout */
- def refresh()
+ def refresh(): Unit =
{
val new_nodes = graphview.visible_graph.topological_order
if (new_nodes != nodes) {
--- a/src/Tools/VSCode/src/build_vscode.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Mon Mar 01 22:22:12 2021 +0100
@@ -17,7 +17,7 @@
/* grammar */
- def build_grammar(options: Options, progress: Progress = new Progress)
+ def build_grammar(options: Options, progress: Progress = new Progress): Unit =
{
val logic = TextMate_Grammar.default_logic
val keywords = Sessions.base_info(options, logic).check.base.overall_syntax.keywords
@@ -30,7 +30,7 @@
/* extension */
- def build_extension(progress: Progress = new Progress, publish: Boolean = false)
+ def build_extension(progress: Progress = new Progress, publish: Boolean = false): Unit =
{
val output_path = extension_dir + Path.explode("out")
progress.echo(output_path.implode)
--- a/src/Tools/VSCode/src/channel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/channel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -61,7 +61,7 @@
/* write message */
- def write(json: JSON.T)
+ def write(json: JSON.T): Unit =
{
val msg = JSON.Format(json)
val content = UTF8.bytes(msg)
@@ -82,17 +82,17 @@
def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
write(LSP.DisplayMessage(message_type, Output.clean_yxml(msg), show))
- def error_message(msg: String) { display_message(LSP.MessageType.Error, msg, true) }
- def warning(msg: String) { display_message(LSP.MessageType.Warning, msg, true) }
- def writeln(msg: String) { display_message(LSP.MessageType.Info, msg, true) }
+ def error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, true)
+ def warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, true)
+ def writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, true)
- def log_error_message(msg: String) { display_message(LSP.MessageType.Error, msg, false) }
- def log_warning(msg: String) { display_message(LSP.MessageType.Warning, msg, false) }
- def log_writeln(msg: String) { display_message(LSP.MessageType.Info, msg, false) }
+ def log_error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, false)
+ def log_warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, false)
+ def log_writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, false)
object Error_Logger extends Logger
{
- def apply(msg: => String) { log_error_message(msg) }
+ def apply(msg: => String): Unit = log_error_message(msg)
}
--- a/src/Tools/VSCode/src/dynamic_output.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala Mon Mar 01 22:22:12 2021 +0100
@@ -50,8 +50,8 @@
{
private val state = Synchronized(Dynamic_Output.State())
- private def handle_update(restriction: Option[Set[Command]])
- { state.change(_.handle_update(server.resources, server.channel, restriction)) }
+ private def handle_update(restriction: Option[Set[Command]]): Unit =
+ state.change(_.handle_update(server.resources, server.channel, restriction))
/* main */
@@ -65,14 +65,14 @@
handle_update(None)
}
- def init()
+ def init(): Unit =
{
server.session.commands_changed += main
server.session.caret_focus += main
handle_update(None)
}
- def exit()
+ def exit(): Unit =
{
server.session.commands_changed -= main
server.session.caret_focus -= main
--- a/src/Tools/VSCode/src/language_server.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/language_server.scala Mon Mar 01 22:22:12 2021 +0100
@@ -81,7 +81,7 @@
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
try {
- System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))
+ System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
server.start()
}
finally { System.setOut(orig_out) }
@@ -142,7 +142,7 @@
private val file_watcher =
File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
- private def close_document(file: JFile)
+ private def close_document(file: JFile): Unit =
{
if (resources.close_model(file)) {
file_watcher.register_parent(file)
@@ -152,17 +152,18 @@
}
}
- private def sync_documents(changed: Set[JFile])
+ private def sync_documents(changed: Set[JFile]): Unit =
{
resources.sync_models(changed)
delay_input.invoke()
delay_output.invoke()
}
- private def change_document(file: JFile, version: Long, changes: List[LSP.TextDocumentChange])
+ private def change_document(
+ file: JFile, version: Long, changes: List[LSP.TextDocumentChange]): Unit =
{
val norm_changes = new mutable.ListBuffer[LSP.TextDocumentChange]
- @tailrec def norm(chs: List[LSP.TextDocumentChange])
+ @tailrec def norm(chs: List[LSP.TextDocumentChange]): Unit =
{
if (chs.nonEmpty) {
val (full_texts, rest1) = chs.span(_.range.isEmpty)
@@ -187,7 +188,7 @@
Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ session.caret_focus.post(Session.Caret_Focus) }
- private def update_caret(caret: Option[(JFile, Line.Position)])
+ private def update_caret(caret: Option[(JFile, Line.Position)]): Unit =
{
resources.update_caret(caret)
delay_caret_update.invoke()
@@ -205,7 +206,7 @@
if (preview_panel.flush(channel)) delay_preview.invoke()
}
- private def request_preview(file: JFile, column: Int)
+ private def request_preview(file: JFile, column: Int): Unit =
{
preview_panel.request(file, column)
delay_preview.invoke()
@@ -220,13 +221,13 @@
if (resources.flush_output(channel)) delay_output.invoke()
}
- def update_output(changed_nodes: Traversable[JFile])
+ def update_output(changed_nodes: Traversable[JFile]): Unit =
{
resources.update_output(changed_nodes)
delay_output.invoke()
}
- def update_output_visible()
+ def update_output_visible(): Unit =
{
resources.update_output_visible()
delay_output.invoke()
@@ -246,15 +247,15 @@
/* init and exit */
- def init(id: LSP.Id)
+ def init(id: LSP.Id): Unit =
{
- def reply_ok(msg: String)
+ def reply_ok(msg: String): Unit =
{
channel.write(LSP.Initialize.reply(id, ""))
channel.writeln(msg)
}
- def reply_error(msg: String)
+ def reply_error(msg: String): Unit =
{
channel.write(LSP.Initialize.reply(id, msg))
channel.error_message(msg)
@@ -313,7 +314,7 @@
}
}
- def shutdown(id: LSP.Id)
+ def shutdown(id: LSP.Id): Unit =
{
def reply(err: String): Unit = channel.write(LSP.Shutdown.reply(id, err))
@@ -341,7 +342,8 @@
})
}
- def exit() {
+ def exit(): Unit =
+ {
log("\n")
sys.exit(if (session_.value.isDefined) 2 else 0)
}
@@ -349,7 +351,7 @@
/* completion */
- def completion(id: LSP.Id, node_pos: Line.Node_Position)
+ def completion(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
@@ -360,7 +362,7 @@
/* spell-checker dictionary */
- def update_dictionary(include: Boolean, permanent: Boolean)
+ def update_dictionary(include: Boolean, permanent: Boolean): Unit =
{
for {
spell_checker <- resources.spell_checker.get
@@ -374,7 +376,7 @@
}
}
- def reset_dictionary()
+ def reset_dictionary(): Unit =
{
for (spell_checker <- resources.spell_checker.get)
{
@@ -386,7 +388,7 @@
/* hover */
- def hover(id: LSP.Id, node_pos: Line.Node_Position)
+ def hover(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
for {
@@ -403,7 +405,7 @@
/* goto definition */
- def goto_definition(id: LSP.Id, node_pos: Line.Node_Position)
+ def goto_definition(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
@@ -414,7 +416,7 @@
/* document highlights */
- def document_highlights(id: LSP.Id, node_pos: Line.Node_Position)
+ def document_highlights(id: LSP.Id, node_pos: Line.Node_Position): Unit =
{
val result =
(for ((rendering, offset) <- rendering_offset(node_pos))
@@ -429,11 +431,11 @@
/* main loop */
- def start()
+ def start(): Unit =
{
log("Server started " + Date.now())
- def handle(json: JSON.T)
+ def handle(json: JSON.T): Unit =
{
try {
json match {
@@ -470,7 +472,7 @@
catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
}
- @tailrec def loop()
+ @tailrec def loop(): Unit =
{
channel.read() match {
case Some(json) =>
@@ -545,7 +547,7 @@
else
snapshot.find_command_position(id, offset).map(node_pos =>
new Hyperlink {
- def follow(unit: Unit) { channel.write(LSP.Caret_Update(node_pos, focus)) }
+ def follow(unit: Unit): Unit = channel.write(LSP.Caret_Update(node_pos, focus))
})
}
--- a/src/Tools/VSCode/src/lsp.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Mon Mar 01 22:22:12 2021 +0100
@@ -21,7 +21,7 @@
{
val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0")
- def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
+ def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean): Unit =
{
val header =
json match {
--- a/src/Tools/VSCode/src/state_panel.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/state_panel.scala Mon Mar 01 22:22:12 2021 +0100
@@ -15,14 +15,14 @@
private val make_id = Counter.make()
private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
- def init(server: Language_Server)
+ def init(server: Language_Server): Unit =
{
val instance = new State_Panel(server)
instances.change(_ + (instance.id -> instance))
instance.init()
}
- def exit(id: Counter.ID)
+ def exit(id: Counter.ID): Unit =
{
instances.change(map =>
map.get(id) match {
@@ -74,9 +74,9 @@
output(content)
})
- def locate() { print_state.locate_query() }
+ def locate(): Unit = print_state.locate_query()
- def update()
+ def update(): Unit =
{
server.editor.current_node_snapshot(()) match {
case Some(snapshot) =>
@@ -93,7 +93,7 @@
private val auto_update_enabled = Synchronized(true)
- def auto_update(set: Option[Boolean] = None)
+ def auto_update(set: Option[Boolean] = None): Unit =
{
val enabled =
auto_update_enabled.guarded_access(a =>
@@ -155,7 +155,7 @@
auto_update()
}
- def init()
+ def init(): Unit =
{
server.session.commands_changed += main
server.session.caret_focus += main
@@ -163,7 +163,7 @@
server.editor.send_dispatcher { auto_update() }
}
- def exit()
+ def exit(): Unit =
{
output_active.change(_ => false)
server.session.commands_changed -= main
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Mar 01 22:22:12 2021 +0100
@@ -160,7 +160,7 @@
file: JFile,
version: Long,
text: String,
- range: Option[Line.Range] = None)
+ range: Option[Line.Range] = None): Unit =
{
state.change(st =>
{
@@ -267,7 +267,7 @@
/* pending input */
- def flush_input(session: Session, channel: Channel)
+ def flush_input(session: Session, channel: Channel): Unit =
{
state.change(st =>
{
@@ -351,8 +351,8 @@
/* caret handling */
- def update_caret(caret: Option[(JFile, Line.Position)])
- { state.change(_.update_caret(caret)) }
+ def update_caret(caret: Option[(JFile, Line.Position)]): Unit =
+ state.change(_.update_caret(caret))
def get_caret(): Option[VSCode_Resources.Caret] =
{
--- a/src/Tools/jEdit/src-base/dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -22,23 +22,23 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- def focusOnDefaultComponent() { JEdit_Lib.request_focus_view(view) }
+ def focusOnDefaultComponent(): Unit = JEdit_Lib.request_focus_view(view)
- def set_content(c: Component) { add(c, BorderLayout.CENTER) }
- def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
+ def set_content(c: Component): Unit = add(c, BorderLayout.CENTER)
+ def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER)
def detach_operation: Option[() => Unit] = None
- protected def init() { }
- protected def exit() { }
+ protected def init(): Unit = {}
+ protected def exit(): Unit = {}
- override def addNotify()
+ override def addNotify(): Unit =
{
super.addNotify()
init()
}
- override def removeNotify()
+ override def removeNotify(): Unit =
{
exit()
super.removeNotify()
--- a/src/Tools/jEdit/src-base/isabelle_encoding.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/isabelle_encoding.scala Mon Mar 01 22:22:12 2021 +0100
@@ -46,13 +46,13 @@
override def getTextWriter(out: OutputStream): Writer =
{
val buffer = new ByteArrayOutputStream(BUFSIZE) {
- override def flush()
+ override def flush(): Unit =
{
val text = Symbol.encode(toString(UTF8.charset_name))
out.write(UTF8.bytes(text))
out.flush()
}
- override def close() { out.close() }
+ override def close(): Unit = out.close()
}
new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
}
--- a/src/Tools/jEdit/src-base/jedit_lib.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala Mon Mar 01 22:22:12 2021 +0100
@@ -14,7 +14,7 @@
object JEdit_Lib
{
- def request_focus_view(alt_view: View = null)
+ def request_focus_view(alt_view: View = null): Unit =
{
val view = if (alt_view != null) alt_view else jEdit.getActiveView()
if (view != null) {
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala Mon Mar 01 22:22:12 2021 +0100
@@ -60,7 +60,7 @@
if (detach_operation.isDefined) {
val detach_item = new JMenuItem("Detach")
detach_item.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
+ def actionPerformed(evt: ActionEvent): Unit = detach_operation.get.apply()
})
menu.add(detach_item)
}
--- a/src/Tools/jEdit/src-base/plugin.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/plugin.scala Mon Mar 01 22:22:12 2021 +0100
@@ -15,7 +15,7 @@
class Plugin extends EBPlugin
{
- override def start()
+ override def start(): Unit =
{
Isabelle_System.init()
@@ -26,10 +26,10 @@
Syntax_Style.dummy_style_extender()
}
- override def stop()
+ override def stop(): Unit =
{
Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
}
- override def handleMessage(message: EBMessage) { }
+ override def handleMessage(message: EBMessage): Unit = {}
}
--- a/src/Tools/jEdit/src-base/syntax_style.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/syntax_style.scala Mon Mar 01 22:22:12 2021 +0100
@@ -31,11 +31,11 @@
}
}
- def set_style_extender(extender: SyntaxUtilities.StyleExtender)
+ def set_style_extender(extender: SyntaxUtilities.StyleExtender): Unit =
{
SyntaxUtilities.setStyleExtender(extender)
GUI_Thread.later { jEdit.propertiesChanged }
}
- def dummy_style_extender() { set_style_extender(Dummy_Extender) }
+ def dummy_style_extender(): Unit = set_style_extender(Dummy_Extender)
}
--- a/src/Tools/jEdit/src/active.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/active.scala Mon Mar 01 22:22:12 2021 +0100
@@ -24,7 +24,7 @@
ServiceManager.getServiceNames(classOf[Handler]).toList
.map(ServiceManager.getService(classOf[Handler], _))
- def action(view: View, text: String, elem: XML.Elem)
+ def action(view: View, text: String, elem: XML.Elem): Unit =
{
GUI_Thread.require {}
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Mar 01 22:22:12 2021 +0100
@@ -74,7 +74,7 @@
case None => false
}
- def exit(text_area: JEditTextArea)
+ def exit(text_area: JEditTextArea): Unit =
{
GUI_Thread.require {}
apply(text_area) match {
@@ -183,7 +183,7 @@
/* completion action: text area */
- private def insert(item: Completion.Item)
+ private def insert(item: Completion.Item): Unit =
{
GUI_Thread.require {}
@@ -239,7 +239,7 @@
val history = PIDE.plugin.completion_history.value
val unicode = Isabelle_Encoding.is_active(buffer)
- def open_popup(result: Completion.Result)
+ def open_popup(result: Completion.Result): Unit =
{
val font =
painter.getFont.deriveFont(
@@ -257,11 +257,13 @@
val completion =
new Completion_Popup(Some(range), layered, loc2, font, items)
{
- override def complete(item: Completion.Item) {
+ override def complete(item: Completion.Item): Unit =
+ {
PIDE.plugin.completion_history.update(item)
insert(item)
}
- override def propagate(evt: KeyEvent) {
+ override def propagate(evt: KeyEvent): Unit =
+ {
if (view.getKeyEventInterceptor == null)
JEdit_Lib.propagate_key(view, evt)
else if (view.getKeyEventInterceptor == inner_key_listener) {
@@ -275,7 +277,8 @@
}
if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
}
- override def shutdown(focus: Boolean) {
+ override def shutdown(focus: Boolean): Unit =
+ {
if (view.getKeyEventInterceptor == inner_key_listener)
view.setKeyEventInterceptor(null)
if (focus) text_area.requestFocus
@@ -342,7 +345,7 @@
/* input key events */
- def input(evt: KeyEvent)
+ def input(evt: KeyEvent): Unit =
{
GUI_Thread.require {}
@@ -400,12 +403,10 @@
private val outer_key_listener =
JEdit_Lib.key_listener(key_typed = input)
- private def activate()
- {
+ private def activate(): Unit =
text_area.addKeyListener(outer_key_listener)
- }
- private def deactivate()
+ private def deactivate(): Unit =
{
dismissed()
text_area.removeKeyListener(outer_key_listener)
@@ -449,7 +450,7 @@
/* insert */
- private def insert(item: Completion.Item)
+ private def insert(item: Completion.Item): Unit =
{
GUI_Thread.require {}
@@ -471,7 +472,7 @@
/* completion action: text field */
- def action()
+ def action(): Unit =
{
GUI.layered_pane(text_field) match {
case Some(layered) if text_field.isEditable =>
@@ -492,14 +493,15 @@
val completion =
new Completion_Popup(None, layered, loc, text_field.getFont, items)
{
- override def complete(item: Completion.Item) {
+ override def complete(item: Completion.Item): Unit =
+ {
PIDE.plugin.completion_history.update(item)
insert(item)
}
- override def propagate(evt: KeyEvent) {
+ override def propagate(evt: KeyEvent): Unit =
if (!evt.isConsumed) text_field.processKeyEvent(evt)
- }
- override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
+ override def shutdown(focus: Boolean): Unit =
+ if (focus) text_field.requestFocus
}
dismissed()
completion_popup = Some(completion)
@@ -514,7 +516,7 @@
/* process key event */
- private def process(evt: KeyEvent)
+ private def process(evt: KeyEvent): Unit =
{
if (PIDE.options.bool("jedit_completion")) {
dismissed()
@@ -534,7 +536,7 @@
action()
}
- override def processKeyEvent(evt0: KeyEvent)
+ override def processKeyEvent(evt0: KeyEvent): Unit =
{
val evt = KeyEventWorkaround.processKeyEvent(evt0)
if (evt != null) {
@@ -574,9 +576,9 @@
/* actions */
- def complete(item: Completion.Item) { }
- def propagate(evt: KeyEvent) { }
- def shutdown(focus: Boolean) { }
+ def complete(item: Completion.Item): Unit = {}
+ def propagate(evt: KeyEvent): Unit = {}
+ def shutdown(focus: Boolean): Unit = {}
/* list view */
@@ -601,7 +603,7 @@
}
}
- private def move_items(n: Int)
+ private def move_items(n: Int): Unit =
{
val i = list_view.peer.getSelectedIndex
val j = ((i + n) min (items.length - 1)) max 0
@@ -611,7 +613,7 @@
}
}
- private def move_pages(n: Int)
+ private def move_pages(n: Int): Unit =
{
val page_size = list_view.peer.getVisibleRowCount - 1
move_items(page_size * n)
@@ -660,14 +662,15 @@
list_view.peer.addKeyListener(inner_key_listener)
list_view.peer.addMouseListener(new MouseAdapter {
- override def mouseClicked(e: MouseEvent) {
+ override def mouseClicked(e: MouseEvent): Unit =
+ {
if (complete_selected()) e.consume
hide_popup()
}
})
list_view.peer.addFocusListener(new FocusAdapter {
- override def focusLost(e: FocusEvent) { hide_popup() }
+ override def focusLost(e: FocusEvent): Unit = hide_popup()
})
@@ -697,13 +700,13 @@
new Popup(layered, completion, screen.relative(layered, size), size)
}
- private def show_popup(focus: Boolean)
+ private def show_popup(focus: Boolean): Unit =
{
popup.show
if (focus) list_view.requestFocus
}
- private def hide_popup()
+ private def hide_popup(): Unit =
{
shutdown(list_view.peer.isFocusOwner)
popup.hide
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -76,7 +76,7 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -84,7 +84,7 @@
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
- private def handle_update()
+ private def handle_update(): Unit =
{
GUI_Thread.require {}
@@ -123,7 +123,7 @@
def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
- private def update_tree(threads: Debugger.Threads)
+ private def update_tree(threads: Debugger.Threads): Unit =
{
val thread_contexts =
(for ((a, b) <- threads.iterator)
@@ -164,7 +164,7 @@
tree.revalidate()
}
- def update_vals()
+ def update_vals(): Unit =
{
tree_selection() match {
case Some(c) if c.stack_state.isDefined =>
@@ -177,14 +177,15 @@
tree.addTreeSelectionListener(
new TreeSelectionListener {
- override def valueChanged(e: TreeSelectionEvent) {
+ override def valueChanged(e: TreeSelectionEvent): Unit =
+ {
update_focus()
update_vals()
}
})
tree.addMouseListener(
new MouseAdapter {
- override def mouseClicked(e: MouseEvent)
+ override def mouseClicked(e: MouseEvent): Unit =
{
val click = tree.getPathForLocation(e.getX, e.getY)
if (click != null && e.getClickCount == 1)
@@ -232,7 +233,7 @@
private val context_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-context")
{
- override def processKeyEvent(evt: KeyEvent)
+ override def processKeyEvent(evt: KeyEvent): Unit =
{
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
eval_expression()
@@ -249,7 +250,7 @@
private val expression_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
{
- override def processKeyEvent(evt: KeyEvent)
+ override def processKeyEvent(evt: KeyEvent): Unit =
{
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
eval_expression()
@@ -266,7 +267,7 @@
reactions += { case ButtonClicked(_) => eval_expression() }
}
- private def eval_expression()
+ private def eval_expression(): Unit =
{
context_field.addCurrentToHistory()
expression_field.addCurrentToHistory()
@@ -297,13 +298,13 @@
/* focus */
- override def focusOnDefaultComponent() { eval_button.requestFocus }
+ override def focusOnDefaultComponent(): Unit = eval_button.requestFocus
addFocusListener(new FocusAdapter {
- override def focusGained(e: FocusEvent) { update_focus() }
+ override def focusGained(e: FocusEvent): Unit = update_focus()
})
- private def update_focus()
+ private def update_focus(): Unit =
{
for (c <- tree_selection()) {
debugger.set_focus(c)
@@ -340,7 +341,7 @@
}
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
PIDE.session.debugger_updates += main
@@ -349,7 +350,7 @@
jEdit.propertiesChanged()
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.global_options -= main
PIDE.session.debugger_updates -= main
@@ -365,7 +366,7 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
}
--- a/src/Tools/jEdit/src/document_model.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Mar 01 22:22:12 2021 +0100
@@ -134,7 +134,7 @@
/* syntax */
- def syntax_changed(names: List[Document.Node.Name])
+ def syntax_changed(names: List[Document.Node.Name]): Unit =
{
GUI_Thread.require {}
@@ -162,7 +162,7 @@
})
}
- def exit(buffer: Buffer)
+ def exit(buffer: Buffer): Unit =
{
GUI_Thread.require {}
state.change(st =>
@@ -174,7 +174,7 @@
else st)
}
- def provide_files(session: Session, files: List[(Document.Node.Name, String)])
+ def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit =
{
GUI_Thread.require {}
state.change(st =>
@@ -190,7 +190,8 @@
if model.node_required
} yield node_name).toSet
- def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false)
+ def node_required(
+ name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
{
GUI_Thread.require {}
@@ -292,7 +293,7 @@
private val plain_text_prefix = "plain_text="
- def open_preview(view: View, plain_text: Boolean)
+ def open_preview(view: View, plain_text: Boolean): Unit =
{
Document_Model.get(view.getBuffer) match {
case Some(model) =>
@@ -497,7 +498,7 @@
// owned by GUI thread
private var _node_required = false
def node_required: Boolean = _node_required
- def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } }
+ def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
def document_view_iterator: Iterator[Document_View] =
for {
@@ -623,13 +624,13 @@
private val buffer_listener: BufferListener = new BufferAdapter
{
override def contentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int)
+ start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
{
pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
}
override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
+ start_line: Int, offset: Int, num_lines: Int, removed_length: Int): Unit =
{
pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
}
@@ -638,7 +639,7 @@
/* syntax */
- def syntax_changed()
+ def syntax_changed(): Unit =
{
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
@@ -647,7 +648,7 @@
buffer.invalidateCachedFoldLevels()
}
- def init_token_marker()
+ def init_token_marker(): Unit =
{
Isabelle.buffer_token_marker(buffer) match {
case Some(marker) if marker != buffer.getTokenMarker =>
--- a/src/Tools/jEdit/src/document_view.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Mar 01 22:22:12 2021 +0100
@@ -34,7 +34,7 @@
}
}
- def exit(text_area: JEditTextArea)
+ def exit(text_area: JEditTextArea): Unit =
{
GUI_Thread.require {}
get(text_area) match {
@@ -109,7 +109,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
// no robust_body
PIDE.editor.invoke_generated()
@@ -123,7 +123,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
rich_text_area.robust_body(()) {
GUI_Thread.assert {}
@@ -190,7 +190,7 @@
}
private val caret_listener = new CaretListener {
- override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
+ override def caretUpdate(e: CaretEvent): Unit = delay_caret_update.invoke()
}
@@ -228,7 +228,7 @@
/* activation */
- private def activate()
+ private def activate(): Unit =
{
val painter = text_area.getPainter
@@ -246,7 +246,7 @@
session.commands_changed += main
}
- private def deactivate()
+ private def deactivate(): Unit =
{
val painter = text_area.getPainter
--- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -49,9 +49,9 @@
tree.setRowHeight(0)
tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
- override def focusOnDefaultComponent() { tree.requestFocusInWindow }
+ override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
- private def action(node: DefaultMutableTreeNode)
+ private def action(node: DefaultMutableTreeNode): Unit =
{
node.getUserObject match {
case Text_File(_, path) =>
@@ -63,7 +63,7 @@
}
tree.addKeyListener(new KeyAdapter {
- override def keyPressed(e: KeyEvent)
+ override def keyPressed(e: KeyEvent): Unit =
{
if (e.getKeyCode == KeyEvent.VK_ENTER) {
e.consume
@@ -78,7 +78,7 @@
}
})
tree.addMouseListener(new MouseAdapter {
- override def mouseClicked(e: MouseEvent)
+ override def mouseClicked(e: MouseEvent): Unit =
{
val click = tree.getPathForLocation(e.getX, e.getY)
if (click != null && e.getClickCount == 1) {
@@ -94,7 +94,7 @@
{
var expand = true
var visible = 0
- def make_visible(row: Int) { visible += 1; tree.expandRow(row) }
+ def make_visible(row: Int): Unit = { visible += 1; tree.expandRow(row) }
for ((entry, row) <- docs.zipWithIndex) {
entry match {
case Doc.Section(_, important) =>
--- a/src/Tools/jEdit/src/font_info.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Mon Mar 01 22:22:12 2021 +0100
@@ -40,7 +40,7 @@
object main_change
{
- private def change_size(change: Float => Float)
+ private def change_size(change: Float => Float): Unit =
{
GUI_Thread.require {}
@@ -72,13 +72,13 @@
})
}
- def step(i: Int)
+ def step(i: Int): Unit =
{
steps += i
delay.invoke()
}
- def reset(size: Float)
+ def reset(size: Float): Unit =
{
delay.revoke()
steps = 0
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -28,7 +28,8 @@
private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph"))
private var implicit_graph = no_graph
- private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
+ private def set_implicit(
+ snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph]): Unit =
{
GUI_Thread.require {}
@@ -71,9 +72,10 @@
private val window_focus_listener =
new WindowFocusListener {
- def windowGainedFocus(e: WindowEvent) {
- Graphview_Dockable.set_implicit(snapshot, graph_result) }
- def windowLostFocus(e: WindowEvent) { Graphview_Dockable.reset_implicit() }
+ def windowGainedFocus(e: WindowEvent): Unit =
+ Graphview_Dockable.set_implicit(snapshot, graph_result)
+ def windowLostFocus(e: WindowEvent): Unit =
+ Graphview_Dockable.reset_implicit()
}
val graphview =
@@ -127,7 +129,7 @@
set_content(graphview)
- override def focusOnDefaultComponent()
+ override def focusOnDefaultComponent(): Unit =
{
graphview match {
case main_panel: isabelle.graphview.Main_Panel =>
@@ -151,13 +153,13 @@
}
}
- override def init()
+ override def init(): Unit =
{
GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main
}
- override def exit()
+ override def exit(): Unit =
{
GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -24,7 +24,8 @@
private var implicit_results = Command.Results.empty
private var implicit_info: XML.Body = Nil
- private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
+ private def set_implicit(
+ snapshot: Document.Snapshot, results: Command.Results, info: XML.Body): Unit =
{
GUI_Thread.require {}
@@ -36,7 +37,8 @@
private def reset_implicit(): Unit =
set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
- def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
+ def apply(
+ view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body): Unit =
{
set_implicit(snapshot, results, info)
view.getDockableWindowManager.floatDockableWindow("isabelle-info")
@@ -54,8 +56,10 @@
private val window_focus_listener =
new WindowFocusListener {
- def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
- def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
+ def windowGainedFocus(e: WindowEvent): Unit =
+ Info_Dockable.set_implicit(snapshot, results, info)
+ def windowLostFocus(e: WindowEvent): Unit =
+ Info_Dockable.reset_implicit()
}
@@ -68,7 +72,7 @@
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -83,8 +87,8 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
private val controls =
@@ -100,14 +104,14 @@
case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
}
- override def init()
+ override def init(): Unit =
{
GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main
handle_resize()
}
- override def exit()
+ override def exit(): Unit =
{
GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/isabelle.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Mar 01 22:22:12 2021 +0100
@@ -202,15 +202,15 @@
}
}
- def set_continuous_checking() { continuous_checking = true }
- def reset_continuous_checking() { continuous_checking = false }
- def toggle_continuous_checking() { continuous_checking = !continuous_checking }
+ def set_continuous_checking(): Unit = { continuous_checking = true }
+ def reset_continuous_checking(): Unit = { continuous_checking = false }
+ def toggle_continuous_checking(): Unit = { continuous_checking = !continuous_checking }
class Continuous_Checking extends CheckBox("Continuous checking")
{
tooltip = "Continuous checking of proof document (visible and required parts)"
reactions += { case ButtonClicked(_) => continuous_checking = selected }
- def load() { selected = continuous_checking }
+ def load(): Unit = { selected = continuous_checking }
load()
}
@@ -223,15 +223,15 @@
/* required document nodes */
- def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
- def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) }
- def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }
+ def set_node_required(view: View): Unit = Document_Model.view_node_required(view, set = true)
+ def reset_node_required(view: View): Unit = Document_Model.view_node_required(view, set = false)
+ def toggle_node_required(view: View): Unit = Document_Model.view_node_required(view, toggle = true)
/* full screen */
// see toggleFullScreen() method in jEdit/org/gjt/sp/jedit/View.java
- def toggle_full_screen(view: View)
+ def toggle_full_screen(view: View): Unit =
{
if (PIDE.options.bool("jedit_toggle_full_screen") ||
Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen()
@@ -257,11 +257,10 @@
/* font size */
- def reset_font_size() {
+ def reset_font_size(): Unit =
Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
- }
- def increase_font_size() { Font_Info.main_change.step(1) }
- def decrease_font_size() { Font_Info.main_change.step(-1) }
+ def increase_font_size(): Unit = Font_Info.main_change.step(1)
+ def decrease_font_size(): Unit = Font_Info.main_change.step(-1)
/* structured edits */
@@ -271,7 +270,7 @@
buffer.getStringProperty("autoIndent") == "full" &&
PIDE.options.bool(option)
- def indent_input(text_area: TextArea)
+ def indent_input(text_area: TextArea): Unit =
{
val buffer = text_area.getBuffer
val line = text_area.getCaretLine
@@ -292,7 +291,7 @@
}
}
- def newline(text_area: TextArea)
+ def newline(text_area: TextArea): Unit =
{
if (!text_area.isEditable()) text_area.getToolkit().beep()
else {
@@ -300,7 +299,7 @@
val line = text_area.getCaretLine
val caret = text_area.getCaretPosition
- def nl { text_area.userInput('\n') }
+ def nl: Unit = text_area.userInput('\n')
if (indent_enabled(buffer, "jedit_indent_newline")) {
buffer_syntax(buffer) match {
@@ -324,7 +323,7 @@
}
}
- def insert_line_padding(text_area: JEditTextArea, text: String)
+ def insert_line_padding(text_area: JEditTextArea, text: String): Unit =
{
val buffer = text_area.getBuffer
JEdit_Lib.buffer_edit(buffer) {
@@ -347,7 +346,7 @@
text_area: TextArea,
padding: Boolean,
id: Document_ID.Generic,
- text: String)
+ text: String): Unit =
{
val buffer = text_area.getBuffer
if (!snapshot.is_outdated && text != "") {
@@ -382,7 +381,7 @@
/* formal entities */
- def goto_entity(view: View)
+ def goto_entity(view: View): Unit =
{
val text_area = view.getTextArea
for {
@@ -393,7 +392,7 @@
} link.info.follow(view)
}
- def select_entity(text_area: JEditTextArea)
+ def select_entity(text_area: JEditTextArea): Unit =
{
for (doc_view <- Document_View.get(text_area)) {
val rendering = doc_view.get_rendering()
@@ -411,49 +410,47 @@
/* completion */
- def complete(view: View, word_only: Boolean)
- {
+ def complete(view: View, word_only: Boolean): Unit =
Completion_Popup.Text_Area.action(view.getTextArea, word_only)
- }
/* control styles */
- def control_sub(text_area: JEditTextArea)
- { Syntax_Style.edit_control_style(text_area, Symbol.sub) }
+ def control_sub(text_area: JEditTextArea): Unit =
+ Syntax_Style.edit_control_style(text_area, Symbol.sub)
- def control_sup(text_area: JEditTextArea)
- { Syntax_Style.edit_control_style(text_area, Symbol.sup) }
+ def control_sup(text_area: JEditTextArea): Unit =
+ Syntax_Style.edit_control_style(text_area, Symbol.sup)
- def control_bold(text_area: JEditTextArea)
- { Syntax_Style.edit_control_style(text_area, Symbol.bold) }
+ def control_bold(text_area: JEditTextArea): Unit =
+ Syntax_Style.edit_control_style(text_area, Symbol.bold)
- def control_emph(text_area: JEditTextArea)
- { Syntax_Style.edit_control_style(text_area, Symbol.emph) }
+ def control_emph(text_area: JEditTextArea): Unit =
+ Syntax_Style.edit_control_style(text_area, Symbol.emph)
- def control_reset(text_area: JEditTextArea)
- { Syntax_Style.edit_control_style(text_area, "") }
+ def control_reset(text_area: JEditTextArea): Unit =
+ Syntax_Style.edit_control_style(text_area, "")
/* block styles */
- private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
+ private def enclose_input(text_area: JEditTextArea, s1: String, s2: String): Unit =
{
s1.foreach(text_area.userInput)
s2.foreach(text_area.userInput)
s2.foreach(_ => text_area.goToPrevCharacter(false))
}
- def input_bsub(text_area: JEditTextArea)
- { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
+ def input_bsub(text_area: JEditTextArea): Unit =
+ enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
- def input_bsup(text_area: JEditTextArea)
- { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
+ def input_bsup(text_area: JEditTextArea): Unit =
+ enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
/* antiquoted cartouche */
- def antiquoted_cartouche(text_area: TextArea)
+ def antiquoted_cartouche(text_area: TextArea): Unit =
{
val buffer = text_area.getBuffer
for {
@@ -484,7 +481,7 @@
/* spell-checker dictionary */
- def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
+ def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean): Unit =
{
for {
spell_checker <- PIDE.plugin.spell_checker.get
@@ -498,7 +495,7 @@
}
}
- def reset_dictionary()
+ def reset_dictionary(): Unit =
{
for (spell_checker <- PIDE.plugin.spell_checker.get)
{
@@ -527,7 +524,7 @@
/* plugin options */
- def plugin_options(frame: Frame)
+ def plugin_options(frame: Frame): Unit =
{
GUI_Thread.require {}
jEdit.setProperty("Plugin Options.last", "isabelle-general")
@@ -552,7 +549,7 @@
/* tooltips */
- def show_tooltip(view: View, control: Boolean)
+ def show_tooltip(view: View, control: Boolean): Unit =
{
GUI_Thread.require {}
@@ -578,7 +575,7 @@
view: View,
range: Text.Range,
avoid_range: Text.Range = Text.Range.offside,
- which: String = "")(get: List[Text.Markup] => Option[Text.Markup])
+ which: String = "")(get: List[Text.Markup] => Option[Text.Markup]): Unit =
{
GUI_Thread.require {}
@@ -601,14 +598,14 @@
def goto_last_error(view: View): Unit =
goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption)
- def goto_prev_error(view: View)
+ def goto_prev_error(view: View): Unit =
{
val caret_range = JEdit_Lib.caret_range(view.getTextArea)
val range = Text.Range(0, caret_range.stop)
goto_error(view, range, avoid_range = caret_range, which = "previous ")(_.lastOption)
}
- def goto_next_error(view: View)
+ def goto_next_error(view: View): Unit =
{
val caret_range = JEdit_Lib.caret_range(view.getTextArea)
val range = Text.Range(caret_range.start, view.getBuffer.getLength)
--- a/src/Tools/jEdit/src/isabelle_export.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_export.scala Mon Mar 01 22:22:12 2021 +0100
@@ -86,7 +86,7 @@
/* open browser */
- def open_browser(view: View)
+ def open_browser(view: View): Unit =
{
val path =
PIDE.maybe_snapshot(view) match {
--- a/src/Tools/jEdit/src/isabelle_options.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Mon Mar 01 22:22:12 2021 +0100
@@ -16,7 +16,7 @@
{
protected val components: List[(String, List[Option_Component])]
- override def _init()
+ override def _init(): Unit =
{
val dummy_property = "options.isabelle.dummy"
@@ -30,7 +30,7 @@
}
}
- override def _save()
+ override def _save(): Unit =
{
for ((_, cs) <- components) cs.foreach(_.save())
}
--- a/src/Tools/jEdit/src/isabelle_session.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_session.scala Mon Mar 01 22:22:12 2021 +0100
@@ -80,7 +80,7 @@
/* open browser */
- def open_browser(view: View)
+ def open_browser(view: View): Unit =
{
val path =
PIDE.maybe_snapshot(view) match {
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Mar 01 22:22:12 2021 +0100
@@ -64,7 +64,7 @@
class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
- swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
+ swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
{
for ((_, entry) <- tree.branches) {
val node = swing_node(Text.Info(entry.range, entry.markup))
@@ -119,7 +119,7 @@
def make_tree(
parent: DefaultMutableTreeNode,
offset: Text.Offset,
- documents: List[Document_Structure.Document])
+ documents: List[Document_Structure.Document]): Unit =
{
(offset /: documents) { case (i, document) =>
document match {
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Mar 01 22:22:12 2021 +0100
@@ -29,7 +29,7 @@
session.update(doc_blobs, edits)
}
override def flush(): Unit = flush_edits()
- def purge() { flush_edits(purge = true) }
+ def purge(): Unit = flush_edits(purge = true)
private val delay1_flush =
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
@@ -105,7 +105,7 @@
/* navigation */
- def push_position(view: View)
+ def push_position(view: View): Unit =
{
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
if (navigator != null) {
@@ -114,7 +114,7 @@
}
}
- def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
+ def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit =
{
GUI_Thread.require {}
@@ -131,7 +131,7 @@
def goto_file(focus: Boolean, view: View, name: String): Unit =
goto_file(focus, view, Line.Node_Position.offside(name))
- def goto_file(focus: Boolean, view: View, pos: Line.Node_Position)
+ def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit =
{
GUI_Thread.require {}
@@ -176,7 +176,7 @@
}
}
- def goto_doc(view: View, path: Path)
+ def goto_doc(view: View, path: Path): Unit =
{
if (path.is_file)
goto_file(true, view, File.platform_path(path))
--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Mar 01 22:22:12 2021 +0100
@@ -98,7 +98,7 @@
def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A =
{
val undo_in_progress = buffer.isUndoInProgress
- def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) }
+ def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
try { set(true); body } finally { set(undo_in_progress) }
}
@@ -196,7 +196,7 @@
else None
}
- def invalidate_range(text_area: TextArea, range: Text.Range)
+ def invalidate_range(text_area: TextArea, range: Text.Range): Unit =
{
val buffer = text_area.getBuffer
buffer_range(buffer).try_restrict(range) match {
@@ -211,7 +211,7 @@
}
}
- def invalidate(text_area: TextArea)
+ def invalidate(text_area: TextArea): Unit =
{
val visible_lines = text_area.getVisibleLines
if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
@@ -316,12 +316,10 @@
/* key event handling */
- def request_focus_view(alt_view: View = null)
- {
+ def request_focus_view(alt_view: View = null): Unit =
isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view)
- }
- def propagate_key(view: View, evt: KeyEvent)
+ def propagate_key(view: View, evt: KeyEvent): Unit =
{
if (view != null && !evt.isConsumed)
view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
@@ -332,7 +330,7 @@
key_pressed: KeyEvent => Unit = _ => (),
key_released: KeyEvent => Unit = _ => ()): KeyListener =
{
- def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
+ def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit =
{
val evt = KeyEventWorkaround.processKeyEvent(evt0)
if (evt != null) handle(evt)
@@ -340,9 +338,9 @@
new KeyListener
{
- def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
- def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
- def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
+ def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed)
+ def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed)
+ def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released)
}
}
--- a/src/Tools/jEdit/src/jedit_options.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala Mon Mar 01 22:22:12 2021 +0100
@@ -44,7 +44,7 @@
PIDE.session.update_options(PIDE.options.value)
}
}
- def load() { selected = stored }
+ def load(): Unit = { selected = stored }
load()
}
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Mar 01 22:22:12 2021 +0100
@@ -125,7 +125,7 @@
private class File_Content(buffer: Buffer) extends
BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
{
- def _run() { }
+ def _run(): Unit = {}
def content(): Bytes =
{
val out = new File_Content_Output(buffer)
@@ -139,7 +139,7 @@
/* theory text edits */
- override def commit(change: Session.Change)
+ override def commit(change: Session.Change): Unit =
{
if (change.syntax_changed.nonEmpty)
GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) }
--- a/src/Tools/jEdit/src/jedit_sessions.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Mar 01 22:22:12 2021 +0100
@@ -134,7 +134,7 @@
infos = PIDE.resources.session_base_info.infos).rc
}
- def session_start(options0: Options)
+ def session_start(options0: Options): Unit =
{
val session = PIDE.session
val options = session_options(options0)
--- a/src/Tools/jEdit/src/keymap_merge.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala Mon Mar 01 22:22:12 2021 +0100
@@ -127,7 +127,7 @@
private def select(head: Int, tail: List[Int], b: Boolean): Unit =
selected.change(set => if (b) set + head -- tail else set - head ++ tail)
- def apply(keymap_name: String, keymap: Keymap)
+ def apply(keymap_name: String, keymap: Keymap): Unit =
{
GUI_Thread.require {}
@@ -164,7 +164,7 @@
override def isCellEditable(row: Int, column: Int): Boolean =
has_entry(row) && column == 0
- override def setValueAt(value: AnyRef, row: Int, column: Int)
+ override def setValueAt(value: AnyRef, row: Int, column: Int): Unit =
{
value match {
case obj: java.lang.Boolean if has_entry(row) && column == 0 =>
@@ -212,7 +212,7 @@
/** check with optional dialog **/
- def check_dialog(view: View)
+ def check_dialog(view: View): Unit =
{
GUI_Thread.require {}
--- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -29,7 +29,7 @@
private var statistics = Queue.empty[Properties.T]
private var statistics_length = 0
- private def add_statistics(stats: Properties.T)
+ private def add_statistics(stats: Properties.T): Unit =
{
statistics = statistics.enqueue(stats)
statistics_length += 1
@@ -42,7 +42,7 @@
case _ =>
}
}
- private def clear_statistics()
+ private def clear_statistics(): Unit =
{
statistics = Queue.empty
statistics_length = 0
@@ -133,12 +133,12 @@
update_delay.invoke()
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.runtime_statistics += main
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.runtime_statistics -= main
}
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -35,7 +35,7 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -43,7 +43,7 @@
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
- private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
+ private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit =
{
GUI_Thread.require {}
@@ -73,7 +73,7 @@
/* controls */
private def output_state: Boolean = PIDE.options.bool("editor_output_state")
- private def output_state_=(b: Boolean)
+ private def output_state_=(b: Boolean): Unit =
{
if (output_state != b) {
PIDE.options.bool("editor_output_state") = b
@@ -131,7 +131,7 @@
GUI_Thread.later { handle_update(do_update, None) }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
PIDE.session.commands_changed += main
@@ -139,7 +139,7 @@
handle_update(true, None)
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
@@ -154,7 +154,7 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
}
--- a/src/Tools/jEdit/src/plugin.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Mon Mar 01 22:22:12 2021 +0100
@@ -92,13 +92,13 @@
/* global changes */
- def options_changed()
+ def options_changed(): Unit =
{
session.global_options.post(Session.Global_Options(options.value))
delay_load.invoke()
}
- def deps_changed()
+ def deps_changed(): Unit =
{
delay_load.invoke()
}
@@ -115,7 +115,7 @@
private val delay_load_active = Synchronized(false)
private def delay_load_activated(): Boolean =
delay_load_active.guarded_access(a => Some((!a, true)))
- private def delay_load_action()
+ private def delay_load_action(): Unit =
{
if (Isabelle.continuous_checking && delay_load_activated() &&
PerspectiveManager.isPerspectiveEnabled)
@@ -229,7 +229,7 @@
/* document model and view */
- def exit_models(buffers: List[Buffer])
+ def exit_models(buffers: List[Buffer]): Unit =
{
GUI_Thread.now {
buffers.foreach(buffer =>
@@ -240,7 +240,7 @@
}
}
- def init_models()
+ def init_models(): Unit =
{
GUI_Thread.now {
PIDE.editor.flush()
@@ -289,13 +289,13 @@
@volatile private var startup_failure: Option[Throwable] = None
@volatile private var startup_notified = false
- private def init_editor(view: View)
+ private def init_editor(view: View): Unit =
{
Keymap_Merge.check_dialog(view)
Session_Build.check_dialog(view)
}
- private def init_title(view: View)
+ private def init_title(view: View): Unit =
{
val title =
proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
@@ -308,7 +308,7 @@
}
}
- override def handleMessage(message: EBMessage)
+ override def handleMessage(message: EBMessage): Unit =
{
GUI_Thread.assert {}
@@ -415,7 +415,7 @@
private var orig_mode_provider: ModeProvider = null
private var pide_mode_provider: ModeProvider = null
- def init_mode_provider()
+ def init_mode_provider(): Unit =
{
orig_mode_provider = ModeProvider.instance
if (orig_mode_provider.isInstanceOf[ModeProvider]) {
@@ -424,7 +424,7 @@
}
}
- def exit_mode_provider()
+ def exit_mode_provider(): Unit =
{
if (ModeProvider.instance == pide_mode_provider)
ModeProvider.instance = orig_mode_provider
@@ -442,7 +442,7 @@
private val shutting_down = Synchronized(false)
- override def start()
+ override def start(): Unit =
{
/* strict initialization */
@@ -481,7 +481,7 @@
if (view != null) init_editor(view)
}
- override def stop()
+ override def stop(): Unit =
{
http_server.stop
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Mar 01 22:22:12 2021 +0100
@@ -53,7 +53,7 @@
def get_background(): Option[Color] = None
- def refresh()
+ def refresh(): Unit =
{
GUI_Thread.require {}
@@ -116,7 +116,7 @@
}
}
- def resize(font_info: Font_Info)
+ def resize(font_info: Font_Info): Unit =
{
GUI_Thread.require {}
@@ -124,7 +124,8 @@
refresh()
}
- def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
+ def update(
+ base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body): Unit =
{
GUI_Thread.require {}
require(!base_snapshot.is_outdated, "document snapshot outdated")
@@ -135,7 +136,7 @@
refresh()
}
- def detach
+ def detach: Unit =
{
GUI_Thread.require {}
Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
@@ -159,9 +160,9 @@
search_action(this)
}
getDocument.addDocumentListener(new DocumentListener {
- def changedUpdate(e: DocumentEvent) { input_delay.invoke() }
- def insertUpdate(e: DocumentEvent) { input_delay.invoke() }
- def removeUpdate(e: DocumentEvent) { input_delay.invoke() }
+ def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke()
+ def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke()
+ def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
})
setColumns(20)
setToolTipText(search_label.tooltip)
@@ -170,7 +171,7 @@
private val search_field_foreground = search_field.foreground
- private def search_action(text_field: JTextField)
+ private def search_action(text_field: JTextField): Unit =
{
val (pattern, ok) =
text_field.getText match {
@@ -197,7 +198,7 @@
new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
override def getAction(action: String): JEditBeanShellAction =
text_area.getActionContext.getAction(action)
- override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean) {}
+ override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {}
override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
})
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Mar 01 22:22:12 2021 +0100
@@ -45,7 +45,7 @@
location: Point,
rendering: JEdit_Rendering,
results: Command.Results,
- info: Text.Info[XML.Body])
+ info: Text.Info[XML.Body]): Unit =
{
GUI_Thread.require {}
@@ -118,7 +118,7 @@
dismiss_unfocused()
}
- def dismiss_unfocused()
+ def dismiss_unfocused(): Unit =
{
stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
case (Nil, _) =>
@@ -129,7 +129,7 @@
}
}
- def dismiss(tip: Pretty_Tooltip)
+ def dismiss(tip: Pretty_Tooltip): Unit =
{
deactivate()
hierarchy(tip) match {
@@ -209,12 +209,12 @@
}
pretty_text_area.addFocusListener(new FocusAdapter {
- override def focusGained(e: FocusEvent)
+ override def focusGained(e: FocusEvent): Unit =
{
tip_border(true)
Pretty_Tooltip.focus_delay.invoke()
}
- override def focusLost(e: FocusEvent)
+ override def focusLost(e: FocusEvent): Unit =
{
tip_border(false)
Pretty_Tooltip.focus_delay.invoke()
@@ -226,7 +226,7 @@
/* main content */
- def tip_border(has_focus: Boolean)
+ def tip_border(has_focus: Boolean): Unit =
{
tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
tip.repaint()
@@ -276,7 +276,7 @@
new Popup(layered, tip, screen.relative(layered, size), size)
}
- private def show_popup
+ private def show_popup: Unit =
{
popup.show
pretty_text_area.requestFocus
--- a/src/Tools/jEdit/src/process_indicator.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/process_indicator.scala Mon Mar 01 22:22:12 2021 +0100
@@ -30,7 +30,8 @@
private var current_frame = 0
private val timer =
new Timer(0, new ActionListener {
- override def actionPerformed(e: ActionEvent) {
+ override def actionPerformed(e: ActionEvent): Unit =
+ {
current_frame = (current_frame + 1) % active_icons.length
setImage(active_icons(current_frame))
label.repaint
@@ -38,7 +39,7 @@
})
timer.setRepeats(true)
- def update(rate: Int)
+ def update(rate: Int): Unit =
{
if (rate == 0) {
setImage(passive_icon)
@@ -59,7 +60,7 @@
def component: Component = label
- def update(tip: String, rate: Int)
+ def update(tip: String, rate: Int): Unit =
{
label.tooltip = tip
animation.update(rate)
--- a/src/Tools/jEdit/src/protocol_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -40,12 +40,12 @@
GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.all_messages += main
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.all_messages -= main
}
--- a/src/Tools/jEdit/src/query_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -42,7 +42,7 @@
: Completion_Popup.History_Text_Field =
new Completion_Popup.History_Text_Field(property)
{
- override def processKeyEvent(evt: KeyEvent)
+ override def processKeyEvent(evt: KeyEvent): Unit =
{
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
super.processKeyEvent(evt)
@@ -56,7 +56,8 @@
/* consume status */
- def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
+ def consume_status(
+ process_indicator: Process_Indicator, status: Query_Operation.Status.Value): Unit =
{
status match {
case Query_Operation.Status.WAITING =>
@@ -83,7 +84,7 @@
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
- private def apply_query()
+ private def apply_query(): Unit =
{
query.addCurrentToHistory()
query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
@@ -125,7 +126,7 @@
process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
- def select { control_panel.contents += zoom }
+ def select: Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Theorems", new BorderPanel {
@@ -149,7 +150,7 @@
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
- private def apply_query()
+ private def apply_query(): Unit =
{
query.addCurrentToHistory()
query_operation.apply_query(List(query.getText))
@@ -175,7 +176,7 @@
query_label, Component.wrap(query), process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
- def select { control_panel.contents += zoom }
+ def select: Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Constants", new BorderPanel {
@@ -231,10 +232,8 @@
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
- private def apply_query()
- {
+ private def apply_query(): Unit =
query_operation.apply_query(selected_items())
- }
private val query_label = new Label("Print:")
def query: JComponent = apply_button.peer
@@ -257,7 +256,7 @@
private val control_panel = Wrap_Panel()
- def select
+ def select: Unit =
{
control_panel.contents.clear
control_panel.contents += query_label
@@ -290,12 +289,16 @@
try { Some(operations(operations_pane.selection.index)) }
catch { case _: IndexOutOfBoundsException => None }
- private def select_operation() {
+ private def select_operation(): Unit =
+ {
for (op <- get_operation()) { op.select; op.query.requestFocus }
operations_pane.revalidate
}
- override def focusOnDefaultComponent() { for (op <- get_operation()) op.query.requestFocus }
+ override def focusOnDefaultComponent(): Unit =
+ {
+ for (op <- get_operation()) op.query.requestFocus
+ }
select_operation()
set_content(operations_pane)
@@ -321,8 +324,8 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
@@ -333,14 +336,14 @@
case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
handle_resize()
operations.foreach(op => op.query_operation.activate())
}
- override def exit()
+ override def exit(): Unit =
{
operations.foreach(op => op.query_operation.deactivate())
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -32,6 +32,6 @@
}
}
- override def init() { PIDE.session.raw_output_messages += main }
- override def exit() { PIDE.session.raw_output_messages -= main }
+ override def init(): Unit = { PIDE.session.raw_output_messages += main }
+ override def exit(): Unit = { PIDE.session.raw_output_messages -= main }
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 01 22:22:12 2021 +0100
@@ -107,7 +107,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
painter_rendering = get_rendering()
painter_clip = gfx.getClip
@@ -123,7 +123,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
painter_rendering = null
painter_clip = null
@@ -131,7 +131,7 @@
}
}
- def robust_rendering(body: JEdit_Rendering => Unit)
+ def robust_rendering(body: JEdit_Rendering => Unit): Unit =
{
robust_body(()) { body(painter_rendering) }
}
@@ -149,7 +149,7 @@
def text_info: Option[(String, Text.Info[A])] = the_text_info
def info: Option[Text.Info[A]] = the_text_info.map(_._2)
- def update(new_info: Option[Text.Info[A]])
+ def update(new_info: Option[Text.Info[A]]): Unit =
{
val old_text_info = the_text_info
val new_text_info =
@@ -173,10 +173,10 @@
}
}
- def update_rendering(r: JEdit_Rendering, range: Text.Range)
- { update(rendering(r)(range)) }
+ def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit =
+ update(rendering(r)(range))
- def reset { update(None) }
+ def reset: Unit = update(None)
}
// owned by GUI thread
@@ -201,16 +201,17 @@
active_areas.exists({ case (area, _) => area.is_active })
private val focus_listener = new FocusAdapter {
- override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
+ override def focusLost(e: FocusEvent): Unit = { robust_body(()) { active_reset() } }
}
private val window_listener = new WindowAdapter {
- override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
- override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
+ override def windowIconified(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
+ override def windowDeactivated(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
}
private val mouse_listener = new MouseAdapter {
- override def mouseClicked(e: MouseEvent) {
+ override def mouseClicked(e: MouseEvent): Unit =
+ {
robust_body(()) {
hyperlink_area.info match {
case Some(Text.Info(range, link)) =>
@@ -246,7 +247,8 @@
}
private val mouse_motion_listener = new MouseMotionAdapter {
- override def mouseDragged(evt: MouseEvent) {
+ override def mouseDragged(evt: MouseEvent): Unit =
+ {
robust_body(()) {
active_reset()
Completion_Popup.Text_Area.dismissed(text_area)
@@ -254,7 +256,8 @@
}
}
- override def mouseMoved(evt: MouseEvent) {
+ override def mouseMoved(evt: MouseEvent): Unit =
+ {
robust_body(()) {
val x = evt.getX
val y = evt.getY
@@ -311,7 +314,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
robust_rendering { rendering =>
val fm = text_area.getPainter.getFontMetrics
@@ -489,7 +492,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
robust_rendering { rendering =>
val painter = text_area.getPainter
@@ -550,7 +553,7 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
{
robust_rendering { rendering =>
val search_pattern = get_search_pattern()
@@ -633,7 +636,7 @@
private class Caret_Painter(before: Boolean) extends TextAreaExtension
{
override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit =
{
robust_rendering { _ =>
if (before) gfx.clipRect(0, 0, 0, 0)
@@ -650,7 +653,7 @@
private val caret_painter = new TextAreaExtension
{
override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit =
{
robust_rendering { rendering =>
if (caret_visible) {
@@ -683,7 +686,7 @@
/* activation */
- def activate()
+ def activate(): Unit =
{
val painter = text_area.getPainter
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
@@ -704,7 +707,7 @@
view.addWindowListener(window_listener)
}
- def deactivate()
+ def deactivate(): Unit =
{
active_reset()
val painter = text_area.getPainter
--- a/src/Tools/jEdit/src/scala_console.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Mon Mar 01 22:22:12 2021 +0100
@@ -28,7 +28,7 @@
{
val buf = new StringBuilder(100)
- override def flush()
+ override def flush(): Unit =
{
val s = buf.synchronized { val s = buf.toString; buf.clear; s }
val str = UTF8.decode_permissive(s)
@@ -39,9 +39,9 @@
Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output
}
- override def close() { flush () }
+ override def close(): Unit = flush()
- def write(byte: Int)
+ def write(byte: Int): Unit =
{
val c = byte.toChar
buf.synchronized { buf.append(c) }
@@ -51,10 +51,10 @@
private val console_writer = new Writer
{
- def flush() { console_stream.flush() }
- def close() { console_stream.flush() }
+ def flush(): Unit = console_stream.flush()
+ def close(): Unit = console_stream.flush()
- def write(cbuf: Array[Char], off: Int, len: Int)
+ def write(cbuf: Array[Char], off: Int, len: Int): Unit =
{
if (len > 0) {
UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
@@ -80,7 +80,7 @@
}
}
- private def report_error(str: String)
+ private def report_error(str: String): Unit =
{
if (global_console == null || global_err == null) isabelle.Output.writeln(str)
else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
@@ -97,7 +97,7 @@
private class Interpreter
{
private val running = Synchronized[Option[Thread]](None)
- def interrupt { 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).
@@ -135,14 +135,14 @@
/* jEdit console methods */
- override def openConsole(console: Console)
+ override def openConsole(console: Console): Unit =
{
val interp = new Interpreter
interp.thread.send(Start(console))
interpreters += (console -> interp)
}
- override def closeConsole(console: Console)
+ override def closeConsole(console: Console): Unit =
{
interpreters.get(console) match {
case Some(interp) =>
@@ -153,7 +153,7 @@
}
}
- override def printInfoMessage(out: Output)
+ override def printInfoMessage(out: Output): Unit =
{
out.print(null,
"This shell evaluates Isabelle/Scala expressions.\n\n" +
@@ -164,19 +164,18 @@
" PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
}
- override def printPrompt(console: Console, out: Output)
+ override def printPrompt(console: Console, out: Output): Unit =
{
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
}
- override def execute(console: Console, input: String, out: Output, err: Output, command: String)
+ override def execute(
+ console: Console, input: String, out: Output, err: Output, command: String): Unit =
{
interpreters(console).thread.send(Execute(console, out, err, command))
}
- override def stop(console: Console)
- {
+ override def stop(console: Console): Unit =
interpreters.get(console).foreach(_.interrupt)
- }
}
--- a/src/Tools/jEdit/src/session_build.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Mon Mar 01 22:22:12 2021 +0100
@@ -21,7 +21,7 @@
object Session_Build
{
- def check_dialog(view: View)
+ def check_dialog(view: View): Unit =
{
val options = PIDE.options.value
Isabelle_Thread.fork() {
@@ -78,7 +78,7 @@
setContentPane(layout_panel.peer)
- private def set_actions(cs: Component*)
+ private def set_actions(cs: Component*): Unit =
{
action_panel.contents.clear
action_panel.contents ++= cs
@@ -108,7 +108,7 @@
}
}
- private def conclude()
+ private def conclude(): Unit =
{
setVisible(false)
dispose()
@@ -120,13 +120,14 @@
setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
addWindowListener(new WindowAdapter {
- override def windowClosing(e: WindowEvent) {
+ override def windowClosing(e: WindowEvent): Unit =
+ {
if (_return_code.isDefined) conclude()
else stopping()
}
})
- private def stopping()
+ private def stopping(): Unit =
{
progress.stop
set_actions(new Label("Stopping ..."))
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -36,7 +36,7 @@
private val text_area = new Pretty_Text_Area(view)
set_content(text_area)
- private def update_contents()
+ private def update_contents(): Unit =
{
val snapshot = current_snapshot
val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
@@ -62,25 +62,22 @@
do_paint()
}
- private def show_trace()
+ private def show_trace(): Unit =
{
val trace = Simplifier_Trace.generate_trace(PIDE.session, current_results)
new Simplifier_Trace_Window(view, current_snapshot, trace)
}
- private def do_paint()
+ private def do_paint(): Unit =
{
GUI_Thread.later {
text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
}
}
- private def handle_resize()
- {
- do_paint()
- }
+ private def handle_resize(): Unit = do_paint()
- private def handle_update(follow: Boolean)
+ private def handle_update(follow: Boolean): Unit =
{
val (new_snapshot, new_command, new_results, new_id) =
PIDE.editor.current_node_snapshot(view) match {
@@ -122,7 +119,7 @@
GUI_Thread.later { handle_update(do_update) }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
PIDE.session.commands_changed += main
@@ -131,7 +128,7 @@
handle_update(true)
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
@@ -147,8 +144,8 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Mar 01 22:22:12 2021 +0100
@@ -159,13 +159,13 @@
open()
do_paint()
- def do_update()
+ def do_update(): Unit =
{
val xml = tree.format
pretty_text_area.update(snapshot, Command.Results.empty, xml)
}
- def do_paint()
+ def do_paint(): Unit =
{
GUI_Thread.later {
pretty_text_area.resize(
@@ -173,10 +173,7 @@
}
}
- def handle_resize()
- {
- do_paint()
- }
+ def handle_resize(): Unit = do_paint()
/* resize */
@@ -185,8 +182,8 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
peer.addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -37,7 +37,7 @@
private val process_indicator = new Process_Indicator
- private def consume_status(status: Query_Operation.Status.Value)
+ private def consume_status(status: Query_Operation.Status.Value): Unit =
{
status match {
case Query_Operation.Status.WAITING =>
@@ -61,11 +61,11 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -76,7 +76,8 @@
/* controls */
- private def clicked {
+ private def clicked: Unit =
+ {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
@@ -91,7 +92,7 @@
}
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
- override def processKeyEvent(evt: KeyEvent)
+ override def processKeyEvent(evt: KeyEvent): Unit =
{
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
super.processKeyEvent(evt)
@@ -100,7 +101,7 @@
setColumns(30)
}
- private def update_provers()
+ private def update_provers(): Unit =
{
val new_provers = PIDE.options.string("sledgehammer_provers")
if (new_provers != provers.getText) {
@@ -144,7 +145,7 @@
add(controls.peer, BorderLayout.NORTH)
- override def focusOnDefaultComponent() { provers.requestFocus }
+ override def focusOnDefaultComponent(): Unit = provers.requestFocus
/* main */
@@ -154,7 +155,7 @@
case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
update_provers()
@@ -162,7 +163,7 @@
sledgehammer.activate()
}
- override def exit()
+ override def exit(): Unit =
{
sledgehammer.deactivate()
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/state_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -43,11 +43,11 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -61,7 +61,7 @@
def update_request(): Unit =
GUI_Thread.require { print_state.apply_query(Nil) }
- def update()
+ def update(): Unit =
{
GUI_Thread.require {}
@@ -126,7 +126,7 @@
GUI_Thread.later { auto_update() }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
PIDE.session.commands_changed += main
@@ -136,7 +136,7 @@
auto_update()
}
- override def exit()
+ override def exit(): Unit =
{
print_state.deactivate()
PIDE.session.caret_focus -= main
--- a/src/Tools/jEdit/src/status_widget.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/status_widget.scala Mon Mar 01 22:22:12 2021 +0100
@@ -50,7 +50,7 @@
def get_status: (String, Double)
- override def paintComponent(gfx: Graphics)
+ override def paintComponent(gfx: Graphics): Unit =
{
super.paintComponent(gfx)
@@ -89,7 +89,7 @@
def action: String
addMouseListener(new MouseAdapter {
- override def mouseClicked(evt: MouseEvent)
+ override def mouseClicked(evt: MouseEvent): Unit =
{
if (evt.getClickCount == 2) {
view.getInputHandler.invokeAction(action)
@@ -114,7 +114,7 @@
status.heap_used_fraction)
}
- private def update_status(new_status: Java_Statistics.Memory_Status)
+ private def update_status(new_status: Java_Statistics.Memory_Status): Unit =
{
if (status != new_status) {
status = new_status
@@ -127,18 +127,17 @@
private val timer =
new Timer(500, new ActionListener {
- override def actionPerformed(e: ActionEvent) {
+ override def actionPerformed(e: ActionEvent): Unit =
update_status(Java_Statistics.memory_status())
- }
})
- override def addNotify()
+ override def addNotify(): Unit =
{
super.addNotify()
timer.start()
}
- override def removeNotify()
+ override def removeNotify(): Unit =
{
super.removeNotify()
timer.stop()
@@ -176,7 +175,7 @@
status.heap_used_fraction)
}
- private def update_status(new_status: ML_Statistics.Memory_Status)
+ private def update_status(new_status: ML_Statistics.Memory_Status): Unit =
{
if (status != new_status) {
status = new_status
@@ -194,13 +193,13 @@
GUI_Thread.later { update_status(status) }
}
- override def addNotify()
+ override def addNotify(): Unit =
{
super.addNotify()
PIDE.session.runtime_statistics += main
}
- override def removeNotify()
+ override def removeNotify(): Unit =
{
super.removeNotify()
PIDE.session.runtime_statistics -= main
--- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -32,7 +32,7 @@
private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
{
- def update_font { font = GUI.font(size = font_size) }
+ def update_font: Unit = { font = GUI.font(size = font_size) }
update_font
text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
@@ -84,7 +84,7 @@
private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
{
- def update_font
+ def update_font: Unit =
{
font =
Symbol.fonts.get(symbol) match {
@@ -183,7 +183,7 @@
/* main */
private val edit_bus_handler: EBComponent =
- new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
+ new EBComponent { def handleMessage(msg: EBMessage): Unit = abbrevs_refresh_delay.invoke() }
private val main =
Session.Consumer[Any](getClass.getName) {
@@ -206,14 +206,14 @@
case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
}
- override def init()
+ override def init(): Unit =
{
EditBus.addToBus(edit_bus_handler)
PIDE.session.global_options += main
PIDE.session.commands_changed += main
}
- override def exit()
+ override def exit(): Unit =
{
EditBus.removeFromBus(edit_bus_handler)
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/syntax_style.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala Mon Mar 01 22:22:12 2021 +0100
@@ -23,7 +23,8 @@
/* extended syntax styles */
private val plain_range: Int = JEditToken.ID_COUNT
- private def check_range(i: Int) { require(0 <= i && i < plain_range, "bad syntax style range") }
+ private def check_range(i: Int): Unit =
+ require(0 <= i && i < plain_range, "bad syntax style range")
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
@@ -107,7 +108,7 @@
def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
{
var result = Map[Text.Offset, Byte => Byte]()
- def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
+ def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit =
{
for (i <- start until stop) result += (i -> style)
}
@@ -148,7 +149,7 @@
/* editing support for control symbols */
- def edit_control_style(text_area: TextArea, control_sym: String)
+ def edit_control_style(text_area: TextArea, control_sym: String): Unit =
{
GUI_Thread.assert {}
--- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -35,13 +35,13 @@
private val main =
Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
- override def init()
+ override def init(): Unit =
{
PIDE.session.syslog_messages += main
syslog_delay.invoke()
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.syslog_messages -= main
}
--- a/src/Tools/jEdit/src/text_overview.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Mar 01 22:22:12 2021 +0100
@@ -33,19 +33,22 @@
setRequestFocusEnabled(false)
addMouseListener(new MouseAdapter {
- override def mousePressed(event: MouseEvent) {
+ override def mousePressed(event: MouseEvent): Unit =
+ {
val line = (event.getY * lines()) / getHeight
if (line >= 0 && line < text_area.getLineCount)
text_area.setCaretPosition(text_area.getLineStartOffset(line))
}
})
- override def addNotify() {
+ override def addNotify(): Unit =
+ {
super.addNotify()
ToolTipManager.sharedInstance.registerComponent(this)
}
- override def removeNotify() {
+ override def removeNotify(): Unit =
+ {
ToolTipManager.sharedInstance.unregisterComponent(this)
super.removeNotify
}
@@ -77,7 +80,7 @@
private val delay_repaint =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
- override def paintComponent(gfx: Graphics)
+ override def paintComponent(gfx: Graphics): Unit =
{
super.paintComponent(gfx)
GUI_Thread.assert {}
--- a/src/Tools/jEdit/src/text_structure.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Mon Mar 01 22:22:12 2021 +0100
@@ -45,7 +45,7 @@
private val keyword_close = Keyword.proof_close
def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
- actions: java.util.List[IndentAction])
+ actions: java.util.List[IndentAction]): Unit =
{
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
@@ -327,7 +327,7 @@
case None => null
}
- def selectMatch(text_area: TextArea)
+ def selectMatch(text_area: TextArea): Unit =
{
def get_span(offset: Text.Offset): Option[Text.Range] =
for {
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -73,7 +73,7 @@
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Status of prover session"
- private def handle_phase(phase: Session.Phase)
+ private def handle_phase(phase: Session.Phase): Unit =
{
GUI_Thread.require {}
session_phase.text = " " + phase_text(phase) + " "
@@ -125,7 +125,7 @@
var checkbox_geometry: Option[(Point, Dimension)] = None
val checkbox = new CheckBox {
opaque = false
- override def paintComponent(gfx: Graphics2D)
+ override def paintComponent(gfx: Graphics2D): Unit =
{
super.paintComponent(gfx)
if (location != null && size != null)
@@ -140,9 +140,9 @@
opaque = false
xAlignment = Alignment.Leading
- override def paintComponent(gfx: Graphics2D)
+ override def paintComponent(gfx: Graphics2D): Unit =
{
- def paint_segment(x: Int, w: Int, color: Color)
+ def paint_segment(x: Int, w: Int, color: Color): Unit =
{
gfx.setColor(color)
gfx.fillRect(x, 0, w, size.height)
@@ -175,7 +175,7 @@
}
}
- def label_border(name: Document.Node.Name)
+ def label_border(name: Document.Node.Name): Unit =
{
val st = nodes_status.overall_node_status(name)
val color =
@@ -210,7 +210,8 @@
}
status.renderer = new Node_Renderer
- private def handle_update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false)
+ private def handle_update(
+ domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit =
{
GUI_Thread.require {}
@@ -250,7 +251,7 @@
GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.phase_changed += main
PIDE.session.global_options += main
@@ -260,7 +261,7 @@
handle_update()
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.phase_changed -= main
PIDE.session.global_options -= main
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -39,9 +39,9 @@
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
var entry: Entry = null
- override def paintComponent(gfx: Graphics2D)
+ override def paintComponent(gfx: Graphics2D): Unit =
{
- def paint_rectangle(color: Color)
+ def paint_rectangle(color: Color): Unit =
{
val size = peer.getSize()
val insets = border.getBorderInsets(peer)
@@ -81,7 +81,7 @@
{
def timing: Double
def print: String
- def follow(snapshot: Document.Snapshot)
+ def follow(snapshot: Document.Snapshot): Unit
}
private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
@@ -89,15 +89,16 @@
{
def print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
- def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
+ def follow(snapshot: Document.Snapshot): Unit =
+ PIDE.editor.goto_file(true, view, name.node)
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
{
def print: String =
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
- def follow(snapshot: Document.Snapshot)
- { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
+ def follow(snapshot: Document.Snapshot): Unit =
+ PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view))
}
@@ -175,7 +176,7 @@
else List(entry))
}
- private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
+ private def handle_update(restriction: Option[Set[Document.Node.Name]] = None): Unit =
{
GUI_Thread.require {}
@@ -211,13 +212,13 @@
GUI_Thread.later { handle_update(Some(changed.nodes)) }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.commands_changed += main
handle_update()
}
- override def exit()
+ override def exit(): Unit =
{
PIDE.session.commands_changed -= main
}
--- a/src/Tools/jEdit/src/token_markup.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Mar 01 22:22:12 2021 +0100
@@ -302,7 +302,7 @@
{
for (mode <- orig_provider.getModes) addMode(mode)
- override def loadMode(mode: Mode, xmh: XModeHandler)
+ override def loadMode(mode: Mode, xmh: XModeHandler): Unit =
{
super.loadMode(mode, xmh)
Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)