tuned --- fewer warnings;
authorwenzelm
Mon, 01 Mar 2021 22:22:12 +0100
changeset 73590 0ffcad1f6130
parent 73589 9efdebe24c65
child 73591 2dd1fd9112d9
tuned --- fewer warnings;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_csdp.scala
src/Pure/Admin/build_cygwin.scala
src/Pure/Admin/build_doc.scala
src/Pure/Admin/build_e.scala
src/Pure/Admin/build_fonts.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_jdk.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_polyml.scala
src/Pure/Admin/build_release.scala
src/Pure/Admin/build_spass.scala
src/Pure/Admin/build_sqlite.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/build_vampire.scala
src/Pure/Admin/build_verit.scala
src/Pure/Admin/build_zipperposition.scala
src/Pure/Admin/check_sources.scala
src/Pure/Admin/components.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/isabelle_devel.scala
src/Pure/Admin/jenkins.scala
src/Pure/Admin/other_isabelle.scala
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/isabelle_thread.scala
src/Pure/GUI/gui.scala
src/Pure/GUI/gui_thread.scala
src/Pure/GUI/popup.scala
src/Pure/GUI/wrap_panel.scala
src/Pure/General/completion.scala
src/Pure/General/csv.scala
src/Pure/General/exn.scala
src/Pure/General/file.scala
src/Pure/General/file_watcher.scala
src/Pure/General/graphics_file.scala
src/Pure/General/http.scala
src/Pure/General/json.scala
src/Pure/General/linear_set.scala
src/Pure/General/logger.scala
src/Pure/General/mercurial.scala
src/Pure/General/multi_map.scala
src/Pure/General/output.scala
src/Pure/General/path.scala
src/Pure/General/scan.scala
src/Pure/General/sql.scala
src/Pure/General/ssh.scala
src/Pure/General/time.scala
src/Pure/General/utf8.scala
src/Pure/Isar/document_structure.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_statistics.scala
src/Pure/PIDE/byte_message.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/editor.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/query_operation.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/xml.scala
src/Pure/PIDE/yxml.scala
src/Pure/System/bash.scala
src/Pure/System/command_line.scala
src/Pure/System/cygwin.scala
src/Pure/System/isabelle_fonts.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/System/linux.scala
src/Pure/System/mingw.scala
src/Pure/System/options.scala
src/Pure/System/posix_interrupt.scala
src/Pure/System/progress.scala
src/Pure/System/scala.scala
src/Pure/System/system_channel.scala
src/Pure/System/tty_loop.scala
src/Pure/Thy/bibtex.scala
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/html.scala
src/Pure/Thy/presentation.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_docker.scala
src/Pure/Tools/build_job.scala
src/Pure/Tools/check_keywords.scala
src/Pure/Tools/debugger.scala
src/Pure/Tools/doc.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/java_monitor.scala
src/Pure/Tools/main.scala
src/Pure/Tools/mkroot.scala
src/Pure/Tools/phabricator.scala
src/Pure/Tools/scala_project.scala
src/Pure/Tools/server.scala
src/Pure/Tools/simplifier_trace.scala
src/Pure/Tools/spell_checker.scala
src/Pure/Tools/update.scala
src/Pure/Tools/update_cartouches.scala
src/Pure/Tools/update_comments.scala
src/Pure/Tools/update_header.scala
src/Pure/Tools/update_then.scala
src/Pure/Tools/update_theorems.scala
src/Tools/Graphview/graph_file.scala
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/graphview.scala
src/Tools/Graphview/main_panel.scala
src/Tools/Graphview/model.scala
src/Tools/Graphview/mutator_dialog.scala
src/Tools/Graphview/mutator_event.scala
src/Tools/Graphview/shapes.scala
src/Tools/Graphview/tree_panel.scala
src/Tools/VSCode/src/build_vscode.scala
src/Tools/VSCode/src/channel.scala
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/language_server.scala
src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/state_panel.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src-base/dockable.scala
src/Tools/jEdit/src-base/isabelle_encoding.scala
src/Tools/jEdit/src-base/jedit_lib.scala
src/Tools/jEdit/src-base/pide_docking_framework.scala
src/Tools/jEdit/src-base/plugin.scala
src/Tools/jEdit/src-base/syntax_style.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_export.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/isabelle_session.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_options.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/keymap_merge.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/process_indicator.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/session_build.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/state_dockable.scala
src/Tools/jEdit/src/status_widget.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/syntax_style.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/text_overview.scala
src/Tools/jEdit/src/text_structure.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
src/Tools/jEdit/src/token_markup.scala
--- 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 ++= "&lt;"
@@ -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 _)