# HG changeset patch
# User wenzelm
# Date 1585342887 -3600
# Node ID 97ccf48c2f0c01924ffaa4f1a6fb6d82bff9c069
# Parent  64aad1e46f98b657c3b465742f1b1ec224658458
misc tuning based on hints by IntelliJ IDEA;

diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/afp.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -166,7 +166,7 @@
   /* dependency graph */
 
   private def sessions_deps(entry: AFP.Entry): List[String] =
-    entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds(_)).distinct.sorted
+    entry.sessions.flatMap(sessions_structure.imports_graph.imm_preds).distinct.sorted
 
   lazy val entries_graph: Graph[String, Unit] =
   {
@@ -214,7 +214,7 @@
       case 1 | 2 =>
         val graph = sessions_structure.build_graph.restrict(sessions.toSet)
         val force_part1 =
-          graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined(_)))).toSet
+          graph.all_preds(graph.all_succs(AFP.force_partition1.filter(graph.defined))).toSet
         val (part1, part2) = graph.keys.partition(a => force_part1(a) || graph.is_isolated(a))
         if (n == 1) part1 else part2
       case _ => error("Bad AFP partition: " + n + " (should be 0, 1, 2)")
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -454,7 +454,7 @@
         "B" -> (_ => multicore_base = true),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
-        "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
+        "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)),
         "N:" -> (arg => isabelle_identifier = arg),
         "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -106,7 +106,7 @@
       }
 
       val dir_entry =
-        File.read_dir(tmp_dir).filterNot(suppress_name(_)) match {
+        File.read_dir(tmp_dir).filterNot(suppress_name) match {
           case List(s) => s
           case _ => error("Archive contains multiple directories")
         }
@@ -232,7 +232,7 @@
       val more_args = getopts(args)
       if (more_args.isEmpty) getopts.usage()
 
-      val archives = more_args.map(Path.explode(_))
+      val archives = more_args.map(Path.explode)
       val progress = new Console_Progress()
 
       build_jdk(archives = archives, progress = progress, target_dir = target_dir)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/build_release.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -163,7 +163,7 @@
       terminate_lines("#bundled components" ::
         (for {
           (catalog, bundled) <- catalogs.iterator
-          val path = Components.admin(dir) + Path.basic(catalog)
+          path = Components.admin(dir) + Path.basic(catalog)
           if path.is_file
           line <- split_lines(File.read(path))
           if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
@@ -196,7 +196,7 @@
             if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
             else None
           case _ => if (Bundled.detect(line)) None else Some(line)
-        }) ::: more_names.map(contrib_name(_)))
+        }) ::: more_names.map(contrib_name))
   }
 
   def make_contrib(dir: Path)
@@ -428,7 +428,6 @@
     val bundle_infos = platform_families.map(release.bundle_info)
 
     for (bundle_info <- bundle_infos) {
-      val bundle_archive = release.dist_dir + bundle_info.path
       val isabelle_name = release.dist_name
       val platform = bundle_info.platform
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/components.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -38,7 +38,7 @@
 
   /* component collections */
 
-  val default_components_base = Path.explode("$ISABELLE_COMPONENTS_BASE")
+  val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
 
   def admin(dir: Path): Path = dir + Path.explode("Admin/components")
 
@@ -125,7 +125,7 @@
         case _ => error("Bad components.sha1 entry: " + quote(line))
       })
 
-  def write_components_sha1(entries: List[SHA1_Digest]) =
+  def write_components_sha1(entries: List[SHA1_Digest]): Unit =
     File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
 
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -18,14 +18,14 @@
   /* global resources: owned by main cronjob */
 
   val backup = "lxbroy10:cronjob"
-  val main_dir = Path.explode("~/cronjob")
-  val main_state_file = main_dir + Path.explode("run/main.state")
-  val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
-  val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
+  val main_dir: Path = Path.explode("~/cronjob")
+  val main_state_file: Path = main_dir + Path.explode("run/main.state")
+  val current_log: Path = main_dir + Path.explode("run/main.log")  // owned by log service
+  val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
 
   val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
-  val isabelle_repos = main_dir + Path.explode("isabelle")
-  val afp_repos = main_dir + Path.explode("AFP")
+  val isabelle_repos: Path = main_dir + Path.explode("isabelle")
+  val afp_repos: Path = main_dir + Path.explode("AFP")
 
   val build_log_dirs =
     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
@@ -42,7 +42,7 @@
   def get_rev(): String = Mercurial.repository(isabelle_repos).id()
   def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
 
-  val init =
+  val init: Logger_Task =
     Logger_Task("init", logger =>
       {
         Isabelle_Devel.make_index()
@@ -61,7 +61,7 @@
           Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
       })
 
-  val exit =
+  val exit: Logger_Task =
     Logger_Task("exit", logger =>
       {
         Isabelle_System.bash(
@@ -72,7 +72,7 @@
 
   /* build release */
 
-  val build_release =
+  val build_release: Logger_Task =
     Logger_Task("build_release", logger =>
       {
         Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
@@ -81,7 +81,7 @@
 
   /* integrity test of build_history vs. build_history_base */
 
-  val build_history_base =
+  val build_history_base: Logger_Task =
     Logger_Task("build_history_base", logger =>
       {
         using(logger.ssh_context.open_session("lxbroy10"))(ssh =>
@@ -414,7 +414,7 @@
 
     def shutdown() { thread.shutdown() }
 
-    val hostname = Isabelle_System.hostname()
+    val hostname: String = Isabelle_System.hostname()
 
     def log(date: Date, task_name: String, msg: String): Unit =
       if (task_name != "")
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -14,8 +14,8 @@
   val BUILD_STATUS = "build_status"
   val CRONJOB_LOG = "cronjob-main.log"
 
-  val root = Path.explode("~/html-data/devel")
-  val cronjob_log = root + Path.basic(CRONJOB_LOG)
+  val root: Path = Path.explode("~/html-data/devel")
+  val cronjob_log: Path = root + Path.basic(CRONJOB_LOG)
 
 
   /* index */
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -43,7 +43,7 @@
     options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
   {
     val store = Sessions.store(options)
-    val infos = job_names.flatMap(build_job_infos(_))
+    val infos = job_names.flatMap(build_job_infos)
     Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -62,7 +62,7 @@
   val etc_preferences: Path = etc + Path.explode("preferences")
 
   def copy_fonts(target_dir: Path): Unit =
-    Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
+    Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
       foreach(entry => File.copy(entry.path, target_dir))
 
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/csv.scala
--- a/src/Pure/General/csv.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/csv.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -20,7 +20,7 @@
 
   sealed case class Record(fields: Any*)
   {
-    override def toString: String = fields.iterator.map(print_field(_)).mkString(",")
+    override def toString: String = fields.iterator.map(print_field).mkString(",")
   }
 
   sealed case class File(name: String, header: List[String], records: List[Record])
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/date.scala
--- a/src/Pure/General/date.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/date.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -33,7 +33,7 @@
     }
 
     def apply(pats: String*): Format =
-      make(pats.toList.map(Date.Formatter.pattern(_)))
+      make(pats.toList.map(Date.Formatter.pattern))
 
     val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
     val date: Format = Format("dd-MMM-uuuu")
@@ -56,7 +56,7 @@
     def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
       pats.flatMap(pat => {
         val fmt = pattern(pat)
-        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
+        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale)
       })
 
     @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/exn.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -70,7 +70,7 @@
   def release_first[A](results: List[Result[A]]): List[A] =
     results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
       case Some(Exn(exn)) => throw exn
-      case _ => results.map(release(_))
+      case _ => results.map(release)
     }
 
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/file.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -213,7 +213,7 @@
     val line =
       try { reader.readLine}
       catch { case _: IOException => null }
-    if (line == null) None else Some(line)
+    Option(line)
   }
 
   def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/graph.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -123,9 +123,9 @@
     (Map.empty[Key, Long] /: xs)(reach(0))
   }
   def node_height(count: Key => Long): Map[Key, Long] =
-    reachable_length(count, imm_preds(_), maximals)
+    reachable_length(count, imm_preds, maximals)
   def node_depth(count: Key => Long): Map[Key, Long] =
-    reachable_length(count, imm_succs(_), minimals)
+    reachable_length(count, imm_succs, minimals)
 
   /*reachable nodes with size limit*/
   def reachable_limit(
@@ -138,7 +138,7 @@
     {
       val (n, rs) = res
       if (rs.contains(x)) res
-      else ((n + count(x), rs + x) /: next(x))(reach _)
+      else ((n + count(x), rs + x) /: next(x))(reach)
     }
 
     @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/json.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -9,6 +9,7 @@
 package isabelle
 
 
+import scala.util.matching.Regex
 import scala.util.parsing.combinator.Parsers
 import scala.util.parsing.combinator.lexical.Scanners
 import scala.util.parsing.input.CharArrayReader.EofCh
@@ -61,14 +62,14 @@
     def errorToken(msg: String): Token = Token(Kind.ERROR, msg)
 
     val white_space: String = " \t\n\r"
-    override val whiteSpace = ("[" + white_space + "]+").r
+    override val whiteSpace: Regex = ("[" + white_space + "]+").r
     def whitespace: Parser[Any] = many(character(white_space.contains(_)))
 
-    val letter: Parser[String] = one(character(Symbol.is_ascii_letter(_)))
-    val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter(_)))
+    val letter: Parser[String] = one(character(Symbol.is_ascii_letter))
+    val letters1: Parser[String] = many1(character(Symbol.is_ascii_letter))
 
-    def digits: Parser[String] = many(character(Symbol.is_ascii_digit(_)))
-    def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit(_)))
+    def digits: Parser[String] = many(character(Symbol.is_ascii_digit))
+    def digits1: Parser[String] = many1(character(Symbol.is_ascii_digit))
 
 
     /* keyword */
@@ -114,8 +115,8 @@
       one(character("eE".contains(_))) ~ maybe(character("-+".contains(_))) ~ digits1 ^^
         { case a ~ b ~ c => a + b + c }
 
-    def zero = one(character(c => c == '0'))
-    def nonzero = one(character(c => c != '0' && Symbol.is_ascii_digit(c)))
+    def zero: Parser[String] = one(character(c => c == '0'))
+    def nonzero: Parser[String] = one(character(c => c != '0' && Symbol.is_ascii_digit(c)))
     def positive: Parser[String] = nonzero ~ digits ^^ { case a ~ b => a + b }
 
 
@@ -326,7 +327,7 @@
     object Seconds
     {
       def unapply(json: T): Option[Time] =
-        Double.unapply(json).map(Time.seconds(_))
+        Double.unapply(json).map(Time.seconds)
     }
   }
 
@@ -402,9 +403,9 @@
     : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default)
 
   def strings(obj: T, name: String): Option[List[String]] =
-    list(obj, name, JSON.Value.String.unapply _)
+    list(obj, name, JSON.Value.String.unapply)
   def strings_default(obj: T, name: String, default: => List[String] = Nil): Option[List[String]] =
-    list_default(obj, name, JSON.Value.String.unapply _, default)
+    list_default(obj, name, JSON.Value.String.unapply, default)
 
   def seconds(obj: T, name: String): Option[Time] =
     value(obj, name, Value.Seconds.unapply)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/linear_set.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -17,7 +17,7 @@
 object Linear_Set extends SetFactory[Linear_Set]
 {
   private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
-  override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
+  override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
 
   implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
   def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/mercurial.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -44,7 +44,7 @@
 
   def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
   {
-    def find(root: Path): Option[Repository] =
+    @tailrec def find(root: Path): Option[Repository] =
       if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
       else if (root.is_root) None
       else find(root + Path.parent)
@@ -95,7 +95,7 @@
     }
 
     def add(files: List[Path]): Unit =
-      hg.command("add", files.map(ssh.bash_path(_)).mkString(" "))
+      hg.command("add", files.map(ssh.bash_path).mkString(" "))
 
     def archive(target: String, rev: String = "", options: String = ""): Unit =
       hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/multi_map.scala
--- a/src/Pure/General/multi_map.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/multi_map.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -14,7 +14,7 @@
 object Multi_Map extends ImmutableMapFactory[Multi_Map]
 {
   private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
-  override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+  override def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
 
   implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
     new MapCanBuildFrom[A, B]
@@ -63,7 +63,7 @@
 
   override def stringPrefix = "Multi_Map"
 
-  override def empty = Multi_Map.empty
+  override def empty: Multi_Map[A, Nothing] = Multi_Map.empty
   override def isEmpty: Boolean = rep.isEmpty
 
   override def keySet: Set[A] = rep.keySet
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/path.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -73,7 +73,7 @@
   val current: Path = new Path(Nil)
   val root: Path = new Path(List(Root("")))
   def named_root(s: String): Path = new Path(List(root_elem(s)))
-  def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
+  def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem))
   def basic(s: String): Path = new Path(List(basic_elem(s)))
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/pretty.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import scala.annotation.tailrec
+
 
 object Pretty
 {
@@ -69,7 +71,7 @@
   {
     val indent1 = force_nat(indent)
 
-    def body_length(prts: List[Tree], len: Double): Double =
+    @tailrec def body_length(prts: List[Tree], len: Double): Double =
     {
       val (line, rest) =
         Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
@@ -104,7 +106,7 @@
 
   private def force_break(tree: Tree): Tree =
     tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
-  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
+  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break)
 
   private def force_next(trees: List[Tree]): List[Tree] =
     trees match {
@@ -113,8 +115,8 @@
       case t :: ts => t :: force_next(ts)
     }
 
-  val default_margin = 76.0
-  val default_breakgain = default_margin / 20
+  val default_margin: Double = 76.0
+  val default_breakgain: Double = default_margin / 20
 
   def formatted(input: XML.Body,
     margin: Double = default_margin,
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/properties.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -67,7 +67,7 @@
         XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text))
       xml_cache match {
         case None => ps
-        case Some(cache) => ps.map(cache.props(_))
+        case Some(cache) => ps.map(cache.props)
       }
     }
   }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/scan.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -10,10 +10,10 @@
 import scala.annotation.tailrec
 import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
 import scala.collection.immutable.PagedSeq
+import scala.util.matching.Regex
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
   Reader, CharSequenceReader}
 import scala.util.parsing.combinator.RegexParsers
-
 import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
 import java.net.URL
 
@@ -39,7 +39,7 @@
 
   trait Parsers extends RegexParsers
   {
-    override val whiteSpace = "".r
+    override val whiteSpace: Regex = "".r
 
 
     /* optional termination */
@@ -237,7 +237,7 @@
     {
       require(depth >= 0)
 
-      val comment_text =
+      val comment_text: Parser[List[String]] =
         rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r)
 
       def apply(in: Input) =
@@ -399,7 +399,7 @@
       else this ++ other.raw_iterator
 
     def -- (remove: Traversable[String]): Lexicon =
-      if (remove.exists(contains(_)))
+      if (remove.exists(contains))
         Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
       else this
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/sql.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -37,7 +37,7 @@
     }
 
   def string(s: String): Source =
-    s.iterator.map(escape_char(_)).mkString("'", "", "'")
+    s.iterator.map(escape_char).mkString("'", "", "'")
 
   def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
@@ -288,7 +288,7 @@
     }
     def date(column: Column): Date = stmt.db.date(res, column)
 
-    def timing(c1: Column, c2: Column, c3: Column) =
+    def timing(c1: Column, c2: Column, c3: Column): Timing =
       Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
 
     def get[A](column: Column, f: Column => A): Option[A] =
@@ -296,13 +296,13 @@
       val x = f(column)
       if (rep.wasNull) None else Some(x)
     }
-    def get_bool(column: Column): Option[Boolean] = get(column, bool _)
-    def get_int(column: Column): Option[Int] = get(column, int _)
-    def get_long(column: Column): Option[Long] = get(column, long _)
-    def get_double(column: Column): Option[Double] = get(column, double _)
-    def get_string(column: Column): Option[String] = get(column, string _)
-    def get_bytes(column: Column): Option[Bytes] = get(column, bytes _)
-    def get_date(column: Column): Option[Date] = get(column, date _)
+    def get_bool(column: Column): Option[Boolean] = get(column, bool)
+    def get_int(column: Column): Option[Int] = get(column, int)
+    def get_long(column: Column): Option[Long] = get(column, long)
+    def get_double(column: Column): Option[Double] = get(column, double)
+    def get_string(column: Column): Option[String] = get(column, string)
+    def get_bytes(column: Column): Option[Bytes] = get(column, bytes)
+    def get_date(column: Column): Option[Date] = get(column, date)
   }
 
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/ssh.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -10,6 +10,7 @@
 import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
 
 import scala.collection.mutable
+import scala.util.matching.Regex
 
 import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException,
   OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS}
@@ -21,7 +22,7 @@
 
   object Target
   {
-    val User_Host = "^([^@]+)@(.+)$".r
+    val User_Host: Regex = "^([^@]+)@(.+)$".r
 
     def parse(s: String): (String, String) =
       s match {
@@ -76,7 +77,7 @@
     jsch.setKnownHosts(File.platform_path(known_hosts))
 
     val identity_files =
-      space_explode(':', options.string("ssh_identity_files")).map(Path.explode(_))
+      space_explode(':', options.string("ssh_identity_files")).map(Path.explode)
     for (identity_file <- identity_files if identity_file.is_file)
       jsch.addIdentity(File.platform_path(identity_file))
 
@@ -431,12 +432,12 @@
     def read_file(path: Path, local_path: Path): Unit =
       sftp.get(remote_path(path), File.platform_path(local_path))
     def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
-    def read(path: Path): String = using(open_input(path))(File.read_stream(_))
+    def read(path: Path): String = using(open_input(path))(File.read_stream)
 
     def write_file(path: Path, local_path: Path): Unit =
       sftp.put(File.platform_path(local_path), remote_path(path))
     def write_bytes(path: Path, bytes: Bytes): Unit =
-      using(open_output(path))(bytes.write_stream(_))
+      using(open_output(path))(bytes.write_stream)
     def write(path: Path, text: String): Unit =
       using(open_output(path))(stream => Bytes(text).write_stream(stream))
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/symbol.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -113,8 +113,8 @@
     {
       private val matcher = new Matcher(text)
       private var i = 0
-      def hasNext = i < text.length
-      def next =
+      def hasNext: Boolean = i < text.length
+      def next: Symbol =
       {
         val n = matcher(i, text.length)
         val s =
@@ -135,10 +135,10 @@
   def length(text: CharSequence): Int = iterator(text).length
 
   def trim_blanks(text: CharSequence): String =
-    Library.trim(is_blank(_), explode(text)).mkString
+    Library.trim(is_blank, explode(text)).mkString
 
   def all_blank(str: String): Boolean =
-    iterator(str).forall(is_blank(_))
+    iterator(str).forall(is_blank)
 
   def trim_blank_lines(text: String): String =
     cat_lines(split_lines(text).dropWhile(all_blank).reverse.dropWhile(all_blank).reverse)
@@ -191,7 +191,7 @@
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
-    def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
+    def decode(symbol_range: Range): Text.Range = symbol_range.map(decode)
 
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
@@ -448,7 +448,7 @@
 
     /* classification */
 
-    val letters = recode_set(
+    val letters: Set[String] = recode_set(
       "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
       "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
       "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
@@ -481,12 +481,12 @@
       "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
       "\\<Psi>", "\\<Omega>")
 
-    val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
+    val blanks: Set[String] = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
 
-    val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
+    val symbolic: Set[String] = recode_set((for {(sym, _) <- symbols; if raw_symbolic(sym)} yield sym): _*)
 
 
     /* misc symbols */
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/url.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -24,7 +24,7 @@
     }
     else c.toString
 
-  def escape_special(s: String): String = s.iterator.map(escape_special(_)).mkString
+  def escape_special(s: String): String = s.iterator.map(escape_special).mkString
 
   def escape_name(name: String): String =
     name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/value.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -70,7 +70,7 @@
       val s = t.seconds
       if (s.toInt.toDouble == s) s.toInt.toString else t.toString
     }
-    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
+    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds)
     def parse(s: java.lang.String): Time =
       unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
   }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/word.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -53,11 +53,11 @@
       }
     def unapply(str: String): Option[Case] =
       if (str.nonEmpty) {
-        if (Codepoint.iterator(str).forall(Character.isLowerCase(_))) Some(Lowercase)
-        else if (Codepoint.iterator(str).forall(Character.isUpperCase(_))) Some(Uppercase)
+        if (Codepoint.iterator(str).forall(Character.isLowerCase)) Some(Lowercase)
+        else if (Codepoint.iterator(str).forall(Character.isUpperCase)) Some(Uppercase)
         else {
           val it = Codepoint.iterator(str)
-          if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase(_)))
+          if (Character.isUpperCase(it.next) && it.forall(Character.isLowerCase))
             Some(Capitalized)
           else None
         }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -169,7 +169,7 @@
       val kinds1 = kinds + (name -> kind)
       val load_commands1 =
         if (kind == THY_LOAD) {
-          if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
+          if (!Symbol.iterator(name).forall(Symbol.is_ascii))
             error("Bad theory load command " + quote(name))
           load_commands + (name -> exts)
         }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Isar/line_structure.scala
--- a/src/Pure/Isar/line_structure.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Isar/line_structure.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -9,7 +9,7 @@
 
 object Line_Structure
 {
-  val init = Line_Structure()
+  val init: Line_Structure = Line_Structure()
 }
 
 sealed case class Line_Structure(
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -193,7 +193,7 @@
       if (tok.is_ignored) ignored += tok
       else if (keywords.is_before_command(tok) ||
         tok.is_command &&
-          (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
+          (!content.exists(keywords.is_before_command) || content.exists(_.is_command)))
       { flush(); content += tok }
       else { content ++= ignored; ignored.clear; content += tok }
     }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Isar/token.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -249,9 +249,9 @@
 
   private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
   {
-    def first = tokens.head
-    def rest = new Token_Reader(tokens.tail, pos.advance(first))
-    def atEnd = tokens.isEmpty
+    def first: Token = tokens.head
+    def rest: Token_Reader = new Token_Reader(tokens.tail, pos.advance(first))
+    def atEnd: Boolean = tokens.isEmpty
   }
 
   def reader(tokens: List[Token], start: Token.Pos): Reader =
@@ -321,8 +321,8 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
-  def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_))
-  def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_))
+  def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword)
+  def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword)
 
   def is_begin: Boolean = is_keyword("begin")
   def is_end: Boolean = is_command("end")
@@ -341,7 +341,7 @@
   {
     val s = content
     is_name && Path.is_wellformed(s) &&
-      !s.exists(Symbol.is_ascii_blank(_)) &&
+      !s.exists(Symbol.is_ascii_blank) &&
       !Path.is_reserved(s)
   }
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -208,7 +208,7 @@
     chart(fields._1, fields._2)
 
   def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
-    fields.map(chart(_)).foreach(c =>
+    fields.map(chart).foreach(c =>
       GUI_Thread.later {
         new Frame {
           iconImage = GUI.isabelle_image()
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/ML/ml_syntax.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -37,13 +37,13 @@
 
   private def print_symbol(s: Symbol.Symbol): String =
     if (s.startsWith("\\<")) s
-    else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
+    else UTF8.bytes(s).iterator.map(print_byte).mkString
 
   def print_string_bytes(str: String): String =
-    quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
+    quote(UTF8.bytes(str).iterator.map(print_byte).mkString)
 
   def print_string_symbols(str: String): String =
-    quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
+    quote(Symbol.iterator(str).map(print_symbol).mkString)
 
 
   /* pair */
@@ -61,5 +61,5 @@
   /* properties */
 
   def print_properties(props: Properties.T): String =
-    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
+    print_list(print_pair(print_string_bytes, print_string_bytes))(props)
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -95,12 +95,12 @@
         copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
     }
 
-    val no_header = Header()
+    val no_header: Header = Header()
     def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name
     {
-      val empty = Name("")
+      val empty: Name = Name("")
 
       object Ordering extends scala.math.Ordering[Name]
       {
@@ -375,7 +375,7 @@
     }
 
     def purge_suppressed: Option[Nodes] =
-      graph.keys_iterator.filter(is_suppressed(_)).toList match {
+      graph.keys_iterator.filter(is_suppressed).toList match {
         case Nil => None
         case del => Some(new Nodes((graph /: del)(_.del_node(_))))
       }
@@ -527,7 +527,7 @@
 
   object Snapshot
   {
-    val init = State.init.snapshot()
+    val init: Snapshot = State.init.snapshot()
   }
 
   abstract class Snapshot
@@ -737,13 +737,13 @@
     {
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
+          val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
           val execs1 = execs + (id -> new_st)
           (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st.accumulate(self_id(st), other_id _, message, xml_cache)
+              val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
               val commands1 = commands + (id -> new_st)
               (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
             case None => fail
@@ -1039,11 +1039,11 @@
 
         /* local node content */
 
-        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+        def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i))
 
-        def convert(range: Text.Range) = range.map(convert(_))
-        def revert(range: Text.Range) = range.map(revert(_))
+        def convert(range: Text.Range): Text.Range = range.map(convert)
+        def revert(range: Text.Range): Text.Range = range.map(revert)
 
         val node_name: Node.Name = name
         val node: Node = version.nodes(name)
@@ -1166,7 +1166,7 @@
                 case some => Some(some)
               }
           }
-          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
+          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
             yield Text.Info(r, x)
         }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/document_id.scala
--- a/src/Pure/PIDE/document_id.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/document_id.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -17,7 +17,7 @@
   type Exec = Generic
 
   val none: Generic = 0
-  val make = Counter.make()
+  val make: Counter = Counter.make()
 
   def apply(id: Generic): String = Value.Long.apply(id)
   def unapply(s: String): Option[Generic] = Value.Long.unapply(s)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/document_status.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -55,7 +55,7 @@
         runs = runs)
     }
 
-    val empty = make(Iterator.empty)
+    val empty: Command_Status = make(Iterator.empty)
 
     def merge(status_iterator: Iterator[Command_Status]): Command_Status =
       if (status_iterator.hasNext) {
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -224,7 +224,7 @@
           }
           else result
 
-        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
+        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory)
 
         (load_theories,
           copy(already_committed = already_committed1, result = result1, load_state = load_state1))
@@ -350,7 +350,7 @@
                     (theory_progress, st.update(nodes_status1))
                   })
 
-              theory_progress.foreach(progress.theory(_))
+              theory_progress.foreach(progress.theory)
 
               check_state()
 
@@ -496,7 +496,7 @@
       lazy val theory_graph: Document.Node.Name.Graph[Unit] =
         Document.Node.Name.make_graph(
           for ((name, theory) <- theories.toList)
-          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
+          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt)))
 
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
 
@@ -542,7 +542,7 @@
         : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) =
       {
         val all_nodes = theory_graph.topological_order
-        val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet
+        val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet
 
         val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
         val (retained, purged) = all_nodes.partition(retain)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -58,8 +58,8 @@
 
   /* basic markup */
 
-  val Empty = Markup("", Nil)
-  val Broken = Markup("broken", Nil)
+  val Empty: Markup = Markup("", Nil)
+  val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -32,7 +32,7 @@
             case a :: bs => (a, bs)
             case _ => throw new XML.XML_Body(body)
           }
-        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
+        Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
@@ -310,7 +310,7 @@
   def define_commands_bulk(commands: List[Command])
   {
     val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
-    irregular.foreach(define_command(_))
+    irregular.foreach(define_command)
     regular match {
       case Nil =>
       case List(command) => define_command(command)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/prover.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -32,14 +32,14 @@
     def properties: Properties.T = message.markup.properties
     def body: XML.Body = message.body
 
-    def is_init = kind == Markup.INIT
-    def is_exit = kind == Markup.EXIT
-    def is_stdout = kind == Markup.STDOUT
-    def is_stderr = kind == Markup.STDERR
-    def is_system = kind == Markup.SYSTEM
-    def is_status = kind == Markup.STATUS
-    def is_report = kind == Markup.REPORT
-    def is_syslog = is_init || is_exit || is_system || is_stderr
+    def is_init: Boolean = kind == Markup.INIT
+    def is_exit: Boolean = kind == Markup.EXIT
+    def is_stdout: Boolean = kind == Markup.STDOUT
+    def is_stderr: Boolean = kind == Markup.STDERR
+    def is_system: Boolean = kind == Markup.SYSTEM
+    def is_status: Boolean = kind == Markup.STATUS
+    def is_report: Boolean = kind == Markup.REPORT
+    def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -21,20 +21,20 @@
     // background
     val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
       markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
-    val background_colors = values
+    val background_colors: ValueSet = values
 
     // foreground
     val quoted, antiquoted = Value
-    val foreground_colors = values -- background_colors
+    val foreground_colors: ValueSet = values -- background_colors
 
     // message underline
     val writeln, information, warning, legacy, error = Value
-    val message_underline_colors = values -- background_colors -- foreground_colors
+    val message_underline_colors: ValueSet = values -- background_colors -- foreground_colors
 
     // message background
     val writeln_message, information_message, tracing_message,
       warning_message, legacy_message, error_message = Value
-    val message_background_colors =
+    val message_background_colors: ValueSet =
       values -- background_colors -- foreground_colors -- message_underline_colors
 
     // text
@@ -42,7 +42,7 @@
       tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
       inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter,
       antiquote, raw_text, plain_text = Value
-    val text_colors =
+    val text_colors: ValueSet =
       values -- background_colors -- foreground_colors -- message_underline_colors --
       message_background_colors
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -213,7 +213,7 @@
   private val _phase = Synchronized[Session.Phase](Session.Inactive)
   private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
 
-  def phase = _phase.value
+  def phase: Session.Phase = _phase.value
   def is_ready: Boolean = phase == Session.Ready
 
 
@@ -645,7 +645,7 @@
           case Session.Change_Flush if prover.defined =>
             val state = global_state.value
             if (!state.removing_versions)
-              postponed_changes.flush(state).foreach(handle_change(_))
+              postponed_changes.flush(state).foreach(handle_change)
 
           case bad =>
             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/xml.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -217,7 +217,7 @@
       else
         lookup(x) match {
           case Some(y) => y
-          case None => x.map(cache_tree(_))
+          case None => x.map(cache_tree)
         }
     }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/yxml.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -21,10 +21,10 @@
   val is_X = (c: Char) => c == X
   val is_Y = (c: Char) => c == Y
 
-  val X_string = X.toString
-  val Y_string = Y.toString
-  val XY_string = X_string + Y_string
-  val XYX_string = XY_string + X_string
+  val X_string: String = X.toString
+  val Y_string: String = Y.toString
+  val XY_string: String = X_string + Y_string
+  val XYX_string: String = XY_string + X_string
 
   def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   def detect_elem(s: String): Boolean = s.startsWith(XY_string)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/bash.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -35,10 +35,10 @@
 
   def string(s: String): String =
     if (s == "") "\"\""
-    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+    else UTF8.bytes(s).iterator.map(bash_chr).mkString
 
   def strings(ss: List[String]): String =
-    ss.iterator.map(Bash.string(_)).mkString(" ")
+    ss.iterator.map(Bash.string).mkString(" ")
 
 
   /* process and result */
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/getopts.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
+
+
 object Getopts
 {
   def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
@@ -44,7 +47,7 @@
         cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
     }
 
-  private def getopts(args: List[List[Char]]): List[List[Char]] =
+  @tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
     args match {
       case List('-', '-') :: rest_args => rest_args
       case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/invoke_scala.scala
--- a/src/Pure/System/invoke_scala.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/invoke_scala.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -123,6 +123,6 @@
 
   val functions =
     List(
-      Markup.INVOKE_SCALA -> invoke_scala _,
-      Markup.CANCEL_SCALA -> cancel_scala _)
+      Markup.INVOKE_SCALA -> invoke_scala,
+      Markup.CANCEL_SCALA -> cancel_scala)
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/numa.scala
--- a/src/Pure/System/numa.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/numa.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -26,7 +26,7 @@
       }
 
     if (numa_nodes_linux.is_file) {
-      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
+      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read)
     }
     else Nil
   }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/options.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -55,7 +55,7 @@
           case word :: rest if word == strip => rest
           case _ => words
         }
-      Word.implode(words1.map(Word.perhaps_capitalize(_)))
+      Word.implode(words1.map(Word.perhaps_capitalize))
     }
 
     def unknown: Boolean = typ == Unknown
@@ -70,19 +70,19 @@
   private val OPTIONS = Path.explode("etc/options")
   private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
 
-  val options_syntax =
+  val options_syntax: Outer_Syntax =
     Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
       (SECTION, Keyword.DOCUMENT_HEADING) +
       (PUBLIC, Keyword.BEFORE_COMMAND) +
       (OPTION, Keyword.THY_DECL)
 
-  val prefs_syntax = Outer_Syntax.empty + "="
+  val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
 
   trait Parser extends Parse.Parser
   {
-    val option_name = atom("option name", _.is_name)
-    val option_type = atom("option type", _.is_name)
-    val option_value =
+    val option_name: Parser[String] = atom("option name", _.is_name)
+    val option_type: Parser[String] = atom("option type", _.is_name)
+    val option_value: Parser[String] =
       opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^
         { case s ~ n => if (s.isDefined) "-" + n else n } |
       atom("option value", tok => tok.is_name || tok.is_float)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/System/progress.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -34,7 +34,7 @@
   def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
 
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
-    Timing.timeit(message, enabled, echo(_))(e)
+    Timing.timeit(message, enabled, echo)(e)
 
   def stopped: Boolean = false
   def interrupt_handler[A](e: => A): A = e
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/export.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -312,7 +312,7 @@
         // list
         if (export_list) {
           (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
-            sorted.foreach(progress.echo(_))
+            sorted.foreach(progress.echo)
         }
 
         // export
@@ -348,7 +348,7 @@
 
   /* Isabelle tool wrapper */
 
-  val default_export_dir = Path.explode("export")
+  val default_export_dir: Path = Path.explode("export")
 
   val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", args =>
   {
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -23,7 +23,7 @@
       else None
 
     def theories: List[Theory] =
-      theory_graph.topological_order.flatMap(theory(_))
+      theory_graph.topological_order.flatMap(theory)
   }
 
   def read_session(
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/file_format.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -56,7 +56,7 @@
 trait File_Format
 {
   def format_name: String
-  override def toString = format_name
+  override def toString: String = format_name
 
   def file_ext: String
   def detect(name: String): Boolean = name.endsWith("." + file_ext)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/html.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -368,7 +368,7 @@
         (if (entry.is_italic) List("  font-style: italic;") else Nil) :::
         List("}"))
 
-    ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face(_)))
+    ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(hidden = true).map(font_face))
       .mkString("", "\n\n", "\n")
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -10,6 +10,7 @@
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
+import scala.util.matching.Regex
 
 
 object Latex
@@ -102,7 +103,7 @@
 
     object File_Line_Error
     {
-      val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
+      val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
       def unapply(line: String): Option[(Path, Int, String)] =
         line match {
           case Pattern(file, Value.Int(line), message) =>
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -235,7 +235,7 @@
                 (Graph_Display.empty_graph /: required_subgraph.topological_order)(
                   { case (g, session) =>
                       val a = session_node(session)
-                      val bs = required_subgraph.imm_preds(session).toList.map(session_node(_))
+                      val bs = required_subgraph.imm_preds(session).toList.map(session_node)
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
               (graph0 /: dependencies.entries)(
@@ -369,7 +369,7 @@
           deps.get(ancestor.get) match {
             case Some(ancestor_base)
             if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) =>
-              ancestor_base.loaded_theories.defined(_)
+              ancestor_base.loaded_theories.defined _
             case _ =>
               error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session))
           }
@@ -652,7 +652,7 @@
 
     def check_sessions(names: List[String])
     {
-      val bad_sessions = SortedSet(names.filterNot(defined(_)): _*).toList
+      val bad_sessions = SortedSet(names.filterNot(defined): _*).toList
       if (bad_sessions.nonEmpty)
         error("Undefined session(s): " + commas_quote(bad_sessions))
     }
@@ -744,8 +744,8 @@
 
   /* parser */
 
-  val ROOT = Path.explode("ROOT")
-  val ROOTS = Path.explode("ROOTS")
+  val ROOT: Path = Path.explode("ROOT")
+  val ROOTS: Path = Path.explode("ROOTS")
 
   private val CHAPTER = "chapter"
   private val SESSION = "session"
@@ -759,7 +759,7 @@
   private val DOCUMENT_FILES = "document_files"
   private val EXPORT_FILES = "export_files"
 
-  val root_syntax =
+  val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
@@ -895,7 +895,7 @@
 
   def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
   {
-    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+    val default_dirs = Isabelle_System.components().filter(is_session_dir)
     for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) }
     yield (select, dir.canonical)
   }
@@ -1073,7 +1073,7 @@
       input_dirs.map(_ + heap(name)).find(_.is_file)
 
     def find_heap_digest(name: String): Option[String] =
-      find_heap(name).flatMap(read_heap_digest(_))
+      find_heap(name).flatMap(read_heap_digest)
 
     def the_heap(name: String): Path =
       find_heap(name) getOrElse
@@ -1105,7 +1105,7 @@
         if (output || has_session_info(db, name)) Some(db) else { db.close; None }
       }
       else if (output) Some(SQLite.open_database(output_database(name)))
-      else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database(_))
+      else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database)
     }
 
     def open_database(name: String, output: Boolean = false): SQL.Database =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -136,7 +136,7 @@
             val new_commands = insert_text(Some(cmd), text) - cmd
             edit_text(rest.toList ::: es, new_commands)
 
-          case Some((cmd, cmd_start)) =>
+          case Some((cmd, _)) =>
             edit_text(es, insert_text(Some(cmd), e.text))
 
           case None =>
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -336,7 +336,7 @@
     {
       val result0 = future_result.join
       val result1 =
-        export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
+        export_consumer.shutdown(close = true).map(Output.error_message_text) match {
           case Nil => result0
           case errs => result0.errors(errs).error_rc
         }
@@ -380,7 +380,7 @@
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
-    val rc =
+    val rc: Int =
       (0 /: results.iterator.map(
         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
     def ok: Boolean = rc == 0
@@ -580,7 +580,7 @@
             }
 
             // messages
-            process_result.err_lines.foreach(progress.echo(_))
+            process_result.err_lines.foreach(progress.echo)
 
             if (process_result.ok)
               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
@@ -594,7 +594,7 @@
             //}}}
           case None if running.size < (max_jobs max 1) =>
             //{{{ check/start next job
-            pending.dequeue(running.isDefinedAt(_)) match {
+            pending.dequeue(running.isDefinedAt) match {
               case Some((name, info)) =>
                 val ancestor_results =
                   deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
@@ -639,7 +639,7 @@
                   store.clean_output(name)
                   using(store.open_database(name, output = true))(store.init_session_info(_, name))
 
-                  val numa_node = numa_nodes.next(used_node(_))
+                  val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Job(progress, name, info, deps, store, do_output, verbose, pide = pide,
                       numa_node, queue.command_timings(name))
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/debugger.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -23,7 +23,7 @@
   {
     def size: Int = debug_states.length + 1
     def reset: Context = copy(index = 0)
-    def select(i: Int) = copy(index = i + 1)
+    def select(i: Int): Context = copy(index = i + 1)
 
     def thread_state: Option[Debug_State] = debug_states.headOption
 
@@ -143,8 +143,8 @@
 
     val functions =
       List(
-        Markup.DEBUGGER_STATE -> debugger_state _,
-        Markup.DEBUGGER_OUTPUT -> debugger_output _)
+        Markup.DEBUGGER_STATE -> debugger_state,
+        Markup.DEBUGGER_OUTPUT -> debugger_output)
   }
 }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/doc.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -46,7 +46,7 @@
 
   private def release_notes(): List[Entry] =
     Section("Release Notes", true) ::
-      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file(_))
+      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file)
 
   private def examples(): List[Entry] =
     Section("Examples", true) ::
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -363,7 +363,7 @@
           session.use_theories(used_theories.map(_.theory),
             unicode_symbols = unicode_symbols,
             progress = progress,
-            commit = Some(Consumer.apply _))
+            commit = Some(Consumer.apply))
 
         val bad_theories = Consumer.shutdown()
         val bad_msgs =
@@ -463,7 +463,7 @@
   Dump cumulative PIDE session database, with the following aspects:
 
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
-      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
+      "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/fontforge.scala
--- a/src/Pure/Tools/fontforge.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/fontforge.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -38,7 +38,7 @@
     }
 
     if (s.nonEmpty && s(0) == '\\') err('\\')
-    s.iterator.map(escape(_)).mkString(q.toString, "", q.toString)
+    s.iterator.map(escape).mkString(q.toString, "", q.toString)
   }
 
   def file_name(path: Path): Script = string(File.standard_path(path))
@@ -121,7 +121,7 @@
     }
 
     def set: Script =
-      List(fontname, familyname, fullname, weight, copyright, fontversion).map(string(_)).
+      List(fontname, familyname, fullname, weight, copyright, fontversion).map(string).
         mkString("SetFontNames(", ",", ")")
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -39,7 +39,7 @@
 
   val daemon_user = "phabricator"
 
-  val sshd_config = Path.explode("/etc/ssh/sshd_config")
+  val sshd_config: Path = Path.explode("/etc/ssh/sshd_config")
 
 
   /* installation parameters */
@@ -59,7 +59,7 @@
 
   val default_mailers: Path = Path.explode("mailers.json")
 
-  val default_system_port = SSH.default_port
+  val default_system_port: Int = SSH.default_port
   val alternative_system_port = 222
   val default_server_port = 2222
 
@@ -69,7 +69,7 @@
 
   /** global configuration **/
 
-  val global_config = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
+  val global_config: Path = Path.explode("/etc/" + isabelle_phabricator_name(ext = "conf"))
 
   def global_config_script(
     init: String = "",
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/print_operation.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -38,6 +38,6 @@
       true
     }
 
-    val functions = List(Markup.PRINT_OPERATIONS -> put _)
+    val functions = List(Markup.PRINT_OPERATIONS -> put)
   }
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -35,8 +35,8 @@
 
     def split(msg: String): (String, String) =
     {
-      val name = msg.takeWhile(is_name_char(_))
-      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
+      val name = msg.takeWhile(is_name_char)
+      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank)
       (name, argument)
     }
 
@@ -607,7 +607,7 @@
         Exn.capture(server_socket.accept) match {
           case Exn.Res(socket) =>
             Standard_Thread.fork("server_connection")
-              { using(Server.Connection(socket))(handle(_)) }
+              { using(Server.Connection(socket))(handle) }
           case Exn.Exn(_) => finished = true
         }
       }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -49,7 +49,7 @@
       : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
     {
       val options = Options.init(prefs = args.preferences, opts = args.options)
-      val dirs = args.dirs.map(Path.explode(_))
+      val dirs = args.dirs.map(Path.explode)
 
       val base_info =
         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -66,8 +66,8 @@
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
-    val lang = path.drop_ext.file_name
-    val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
+    val lang: String = path.drop_ext.file_name
+    val user_path: Path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/Tools/update_cartouches.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -7,13 +7,16 @@
 package isabelle
 
 
+import scala.util.matching.Regex
+
+
 object Update_Cartouches
 {
   /* update cartouches */
 
   private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
 
-  val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
+  val Text_Antiq: Regex = """(?s)@\{\s*text\b\s*(.+)\}""".r
 
   def update_text(content: String): String =
   {
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/library.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -140,7 +140,7 @@
     else s
 
   def trim_split_lines(s: String): List[String] =
-    split_lines(trim_line(s)).map(trim_line(_))
+    split_lines(trim_line(s)).map(trim_line)
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
@@ -204,7 +204,7 @@
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
-    if (s.exists(is_regex_meta(_))) {
+    if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/term.scala
--- a/src/Pure/term.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/term.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -50,7 +50,7 @@
     override def toString: String =
       "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
   }
-  val dummyT = Type("dummy")
+  val dummyT: Type = Type("dummy")
 
   sealed abstract class Term
   {
@@ -143,7 +143,7 @@
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
     protected def cache_sort(x: Sort): Sort =
-      if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string(_)))
+      if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string))
 
     protected def cache_typ(x: Typ): Typ =
     {
@@ -166,7 +166,7 @@
       else {
         lookup(x) match {
           case Some(y) => y
-          case None => store(x.map(cache_typ(_)))
+          case None => store(x.map(cache_typ))
         }
       }
     }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/graph_file.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -30,8 +30,8 @@
     }
 
     val name = file.getName
-    if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
-    else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
+    if (name.endsWith(".png")) Graphics_File.write_png(file, paint, w, h)
+    else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint, w, h)
     else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/graphview.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -82,7 +82,7 @@
       }
       else node.toString
 
-    _layout = Layout.make(options, metrics, node_text _, visible_graph)
+    _layout = Layout.make(options, metrics, node_text, visible_graph)
   }
 
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/layout.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -104,7 +104,7 @@
                 val lines = split_lines(node_text(a, content))
                 val w2 = metrics.node_width2(lines)
                 val h2 = metrics.node_height2(lines.length)
-                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node(_)))
+                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
             }).toList)
 
       val initial_levels: Levels =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/model.scala
--- a/src/Tools/Graphview/model.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/model.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -18,7 +18,7 @@
   val events = new Mutator_Event.Bus
 
   private var _mutators : List[Mutator.Info] = Nil
-  def apply() = _mutators
+  def apply(): List[Mutator.Info] = _mutators
   def apply(mutators: List[Mutator.Info])
   {
     _mutators = mutators
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/mutator.scala
--- a/src/Tools/Graphview/mutator.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/mutator.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -173,6 +173,6 @@
 
 trait Filter extends Mutator
 {
-  def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
+  def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph = filter(graph)
   def filter(graph: Graph_Display.Graph): Graph_Display.Graph
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -110,7 +110,7 @@
     filter_panel.repaint
   }
 
-  val filter_panel = new BoxPanel(Orientation.Vertical) {}
+  val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {}
 
   private val mutator_box = new ComboBox[Mutator](container.available)
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -23,7 +23,7 @@
   def generate(keywords: Keyword.Keywords): JSON.S =
   {
     val (minor_keywords, operators) =
-      keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier(_))
+      keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier)
 
     def major_keywords(pred: String => Boolean): List[String] =
       (for {
@@ -39,7 +39,7 @@
 
 
     def grouped_names(as: List[String]): String =
-      JSON.Format("\\b(" + as.sorted.map(Library.escape_regex(_)).mkString("|") + ")\\b")
+      JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b")
 
     """{
   "name": "Isabelle",
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -140,7 +140,7 @@
     }
 
   private val file_watcher =
-    File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
+    File_Watcher(sync_documents, options.seconds("vscode_load_delay"))
 
   private def close_document(file: JFile)
   {
@@ -486,7 +486,7 @@
       channel.read() match {
         case Some(json) =>
           json match {
-            case bulk: List[_] => bulk.foreach(handle(_))
+            case bulk: List[_] => bulk.foreach(handle)
             case _ => handle(json)
           }
           loop()
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Color, Font, Point, BorderLayout, Dimension}
-import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
+import java.awt.event.{KeyEvent, KeyListener, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import java.io.{File => JFile}
 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
 import javax.swing.border.LineBorder
@@ -18,7 +18,6 @@
 
 import scala.swing.{ListView, ScrollPane}
 import scala.swing.event.MouseClicked
-
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
 import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
@@ -399,7 +398,7 @@
     /* activation */
 
     private val outer_key_listener =
-      JEdit_Lib.key_listener(key_typed = input _)
+      JEdit_Lib.key_listener(key_typed = input)
 
     private def activate()
     {
@@ -570,7 +569,7 @@
   GUI_Thread.require {}
 
   require(items.nonEmpty)
-  val multi = items.length > 1
+  val multi: Boolean = items.length > 1
 
 
   /* actions */
@@ -621,7 +620,7 @@
 
   /* event handling */
 
-  val inner_key_listener =
+  val inner_key_listener: KeyListener =
     JEdit_Lib.key_listener(
       key_pressed = (e: KeyEvent) =>
         {
@@ -655,7 +654,7 @@
           }
           propagate(e)
         },
-      key_typed = propagate _
+      key_typed = propagate
     )
 
   list_view.peer.addKeyListener(inner_key_listener)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -74,7 +74,7 @@
 
   val pretty_text_area = new Pretty_Text_Area(view)
 
-  override def detach_operation = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
   private def handle_resize()
   {
@@ -208,22 +208,22 @@
 
   private val continue_button = new Button("Continue") {
     tooltip = "Continue program on current thread, until next breakpoint"
-    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue) }
   }
 
   private val step_button = new Button("Step") {
     tooltip = "Single-step in depth-first order"
-    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step) }
   }
 
   private val step_over_button = new Button("Step over") {
     tooltip = "Single-step within this function"
-    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over) }
   }
 
   private val step_out_button = new Button("Step out") {
     tooltip = "Single-step outside this function"
-    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out(_)) }
+    reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out) }
   }
 
   private val context_label = new Label("Context:") {
@@ -318,7 +318,7 @@
 
   /* main panel */
 
-  val main_panel = new SplitPane(Orientation.Vertical) {
+  val main_panel: SplitPane = new SplitPane(Orientation.Vertical) {
     oneTouchExpandable = true
     leftComponent = tree_pane
     rightComponent = Component.wrap(pretty_text_area)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -81,7 +81,7 @@
   private val state = Synchronized(State())  // owned by GUI thread
 
   def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
-  def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
+  def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
   def document_blobs(): Document.Blobs = state.value.document_blobs
@@ -313,7 +313,7 @@
     val preview =
       HTTP.get(preview_root, arg =>
         for {
-          query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_))
+          query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
           name = Library.perhaps_unprefix(plain_text_prefix, query)
           model <- get(PIDE.resources.node_name(name))
         }
@@ -348,7 +348,7 @@
         if (hidden) Text.Perspective.empty
         else {
           val view_ranges = document_view_ranges(snapshot)
-          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
+          val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
           Text.Perspective(view_ranges ::: load_ranges)
         }
       val overlays = PIDE.editor.node_overlays(node_name)
@@ -589,7 +589,7 @@
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear
           last_perspective = perspective
-          node_edits(node_header, edits, perspective)
+          node_edits(node_header(), edits, perspective)
         }
         else Nil
       }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -137,7 +137,7 @@
         JEdit_Lib.buffer_lock(buffer) {
           val rendering = get_rendering()
 
-          for (i <- 0 until physical_lines.length) {
+          for (i <- physical_lines.indices) {
             if (physical_lines(i) != -1) {
               val line_range = Text.Range(start(i), end(i))
 
@@ -241,7 +241,7 @@
     text_area.revalidate()
     text_area.repaint()
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
-      foreach(text_area.addStructureMatcher(_))
+      foreach(text_area.addStructureMatcher)
     session.raw_edits += main
     session.commands_changed += main
   }
@@ -253,7 +253,7 @@
     session.raw_edits -= main
     session.commands_changed -= main
     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
-      foreach(text_area.removeStructureMatcher(_))
+      foreach(text_area.removeStructureMatcher)
     text_overview.foreach(_.revoke())
     text_overview.foreach(text_area.removeLeftOfScrollBar(_))
     text_area.removeCaretListener(caret_listener)
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -406,8 +406,8 @@
 
   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   {
-    s1.foreach(text_area.userInput(_))
-    s2.foreach(text_area.userInput(_))
+    s1.foreach(text_area.userInput)
+    s2.foreach(text_area.userInput)
     s2.foreach(_ => text_area.goToPrevCharacter(false))
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -39,7 +39,7 @@
 
 class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
 {
-  val options = PIDE.options
+  val options: JEdit_Options = PIDE.options
 
   private val predefined =
     List(JEdit_Sessions.logic_selector(options, false),
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -53,11 +53,11 @@
     }
     override def getLongString: String = _name
     override def getName: String = _name
-    override def setName(name: String) = _name = name
+    override def setName(name: String): Unit = _name = name
     override def getStart: Position = _start
-    override def setStart(start: Position) = _start = start
+    override def setStart(start: Position): Unit = _start = start
     override def getEnd: Position = _end
-    override def setEnd(end: Position) = _end = end
+    override def setEnd(end: Position): Unit = _end = end
     override def toString: String = _name
   }
 
@@ -148,19 +148,19 @@
 
 class Isabelle_Sidekick_Default extends
   Isabelle_Sidekick_Structure("isabelle",
-    PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
+    PIDE.resources.theory_node_name, Document_Structure.parse_sections)
 
 class Isabelle_Sidekick_Context extends
   Isabelle_Sidekick_Structure("isabelle-context",
-    PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
+    PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
 
 class Isabelle_Sidekick_Options extends
   Isabelle_Sidekick_Structure("isabelle-options",
-    _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
+    _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
 
 class Isabelle_Sidekick_Root extends
   Isabelle_Sidekick_Structure("isabelle-root",
-    _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
+    _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
 
 class Isabelle_Sidekick_ML extends
   Isabelle_Sidekick_Structure("isabelle-ml",
@@ -257,7 +257,7 @@
         case _ =>
       }
       offset += line.length + 1
-      if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
+      if (!line.forall(Character.isSpaceChar)) end_offset = offset
     }
     if (!stopped) { close2; close1 }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/isabelle_vfs.scala
--- a/src/Tools/jEdit/src/isabelle_vfs.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -77,7 +77,7 @@
     else {
       val files = _listFiles(vfs_session, parent, component)
       if (files == null) null
-      else files.find(_.getPath == url) getOrElse null
+      else files.find(_.getPath == url).orNull
     }
   }
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -202,7 +202,7 @@
       case doc: Doc.Text_File if doc.name == name => doc.path
       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
         new Hyperlink {
-          override val external = !path.is_file
+          override val external: Boolean = !path.is_file
           def follow(view: View): Unit = goto_doc(view, path)
           override def toString: String = "doc " + quote(name)
         })
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -160,7 +160,7 @@
     else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
 
   def jedit_text_areas(): Iterator[JEditTextArea] =
-    jedit_views().flatMap(jedit_text_areas(_))
+    jedit_views().flatMap(jedit_text_areas)
 
   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
     jedit_text_areas().filter(_.getBuffer == buffer)
@@ -319,8 +319,8 @@
       def string_width(s: String): Double =
         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
 
-      val unit = string_width(Symbol.space) max 1.0
-      val average = string_width("mix") / (3 * unit)
+      val unit: Double = string_width(Symbol.space) max 1.0
+      val average: Double = string_width("mix") / (3 * unit)
       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -129,7 +129,7 @@
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil
       }
     value.sections.sortBy(_._1).map(
-        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component _)) })
+        { case (a, opts) => (a, opts.sortBy(_.title("jedit")).flatMap(mk_component)) })
       .filterNot(_._2.isEmpty)
   }
 }
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -300,11 +300,11 @@
   def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
   {
     val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
-    tooltips(elements, range).map(info => info.map(Pretty.fbreaks(_)))
+    tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
   }
 
-  lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
-  lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
+  lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
+  lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
 
 
   /* gutter */
@@ -378,7 +378,7 @@
     else
       snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
         {
-          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_))
+          case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
         })
   }
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -37,7 +37,7 @@
   /* document node name */
 
   def node_name(path: String): Document.Node.Name =
-    JEdit_Lib.check_file(path).flatMap(find_theory(_)) getOrElse {
+    JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse {
       val vfs = VFSManager.getVFSForPath(path)
       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -32,7 +32,7 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  override def detach_operation = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
 
   private def handle_resize()
@@ -58,7 +58,7 @@
         }
 
       val new_output =
-        if (!restriction.isDefined || restriction.get.contains(command))
+        if (restriction.isEmpty || restriction.get.contains(command))
           Rendering.output_messages(results)
         else current_output
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -150,7 +150,7 @@
             }
             else Nil
 
-          (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt(_))
+          (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
         }
         if (required_files.nonEmpty) {
           try {
@@ -184,7 +184,7 @@
     if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
 
   lazy val file_watcher: File_Watcher =
-    File_Watcher(file_watcher_action _, options.seconds("editor_load_delay"))
+    File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
 
 
   /* session phase */
@@ -460,11 +460,11 @@
       completion_history.load()
       spell_checker.update(options.value)
 
-      JEdit_Lib.jedit_views.foreach(init_title(_))
+      JEdit_Lib.jedit_views.foreach(init_title)
 
       isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
       init_mode_provider()
-      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
+      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init)
 
       http_server.start
 
@@ -489,7 +489,7 @@
 
     isabelle.jedit_base.Syntax_Style.dummy_style_extender()
     exit_mode_provider()
-    JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
+    JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit)
 
     if (startup_failure.isEmpty) {
       options.value.save_prefs()
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -146,7 +146,7 @@
   }
 
   def dismiss_descendant(parent: JComponent): Unit =
-    descendant(parent).foreach(dismiss(_))
+    descendant(parent).foreach(dismiss)
 
   def dismissed_all(): Boolean =
   {
@@ -203,7 +203,7 @@
 
   /* text area */
 
-  val pretty_text_area =
+  val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
       override def get_background() = Some(rendering.tooltip_color)
     }
@@ -262,7 +262,7 @@
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
       val lines =
         XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
-          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
+          (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -302,7 +302,7 @@
   select_operation()
   set_content(operations_pane)
 
-  override def detach_operation =
+  override def detach_operation: Option[() => Unit] =
     get_operation() match {
       case None => None
       case Some(op) => op.pretty_text_area.detach_operation
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -159,15 +159,15 @@
 
   private val highlight_area =
     new Active_Area[Color](
-      (rendering: JEdit_Rendering) => rendering.highlight _, None)
+      (rendering: JEdit_Rendering) => rendering.highlight, None)
 
   private val hyperlink_area =
     new Active_Area[PIDE.editor.Hyperlink](
-      (rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
+      (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR))
 
   private val active_area =
     new Active_Area[XML.Elem](
-      (rendering: JEdit_Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR))
+      (rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR))
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (active_area, false))
@@ -292,7 +292,7 @@
       robust_rendering { rendering =>
         val fm = text_area.getPainter.getFontMetrics
 
-        for (i <- 0 until physical_lines.length) {
+        for (i <- physical_lines.indices) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
@@ -479,7 +479,7 @@
           ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
         }
 
-        for (i <- 0 until physical_lines.length) {
+        for (i <- physical_lines.indices) {
           val line = physical_lines(i)
           if (line != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
@@ -525,7 +525,7 @@
     {
       robust_rendering { rendering =>
         val search_pattern = get_search_pattern()
-        for (i <- 0 until physical_lines.length) {
+        for (i <- physical_lines.indices) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -30,7 +30,7 @@
     def find_jars(start: String): List[String] =
       if (start != null)
         File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
-          map(File.absolute_name(_))
+          map(File.absolute_name)
       else Nil
 
     val initial_class_path =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -40,7 +40,7 @@
 
   private class Dialog(view: View) extends JDialog(view)
   {
-    val options = PIDE.options.value
+    val options: Options = PIDE.options.value
 
 
     /* text */
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -30,7 +30,7 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  override def detach_operation = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
 
   /* query operation */
@@ -50,7 +50,7 @@
   }
 
   private val sledgehammer =
-    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
+    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
       (snapshot, results, body) =>
         pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -29,7 +29,7 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  override def detach_operation = pretty_text_area.detach_operation
+  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
   private val print_state =
     new Query_Operation(PIDE.editor, view, "print_state", _ => (),
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -174,7 +174,7 @@
     }
 
     for (page <- pages)
-      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
+      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize))
   }
   set_content(group_tabs)
 
@@ -200,7 +200,7 @@
                 }
               case _ =>
             })
-          comp.revalidate
+          comp.revalidate()
           comp.repaint()
         }
       case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -99,9 +99,9 @@
   }
 
   private def control_style(sym: String): Option[Byte => Byte] =
-    if (sym == Symbol.sub_decoded) Some(subscript(_))
-    else if (sym == Symbol.sup_decoded) Some(superscript(_))
-    else if (sym == Symbol.bold_decoded) Some(bold(_))
+    if (sym == Symbol.sub_decoded) Some(subscript)
+    else if (sym == Symbol.sup_decoded) Some(superscript)
+    else if (sym == Symbol.bold_decoded) Some(bold)
     else None
 
   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -21,7 +21,7 @@
 
   class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean)
   {
-    val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+    val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0
 
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
@@ -137,7 +137,7 @@
                   else i })
 
           def indent_extra: Int =
-            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
+            if (prev_span.exists(keywords.is_quasi_command)) indent_size
             else 0
 
           val indent =