# HG changeset patch
# User wenzelm
# Date 1626556194 -7200
# Node ID c13198575f755af3c8c6d85d0ba9e6fb580c259e
# Parent  57768f30d17c4361199ad02a8ab1d88886fc64dd
tuned --- based on hints by IntelliJ IDEA;

diff -r 57768f30d17c -r c13198575f75 src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala	Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Pure/System/getopts.scala	Sat Jul 17 23:09:54 2021 +0200
@@ -18,8 +18,8 @@
       option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
         case (m, (s, f)) =>
           val (a, entry) =
-            if (s.size == 1) (s(0), (false, f))
-            else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
+            if (s.length == 1) (s(0), (false, f))
+            else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f))
             else error("Bad option specification: " + quote(s))
           if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
           else m + (a -> entry)
diff -r 57768f30d17c -r c13198575f75 src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala	Sat Jul 17 23:09:54 2021 +0200
@@ -13,7 +13,7 @@
 
 import javax.swing.tree.DefaultMutableTreeNode
 import javax.swing.text.Position
-import javax.swing.{JLabel, Icon}
+import javax.swing.Icon
 
 import org.gjt.sp.jedit.Buffer
 import sidekick.{SideKickParser, SideKickParsedData, IAsset}
@@ -22,7 +22,10 @@
 object Isabelle_Sidekick
 {
   def int_to_pos(offset: Text.Offset): Position =
-    new Position { def getOffset = offset; override def toString: String = offset.toString }
+    new Position {
+      def getOffset: Text.Offset = offset
+      override def toString: String = offset.toString
+    }
 
   def root_data(buffer: Buffer): SideKickParsedData =
   {
@@ -35,9 +38,9 @@
   {
     private val css = GUI.imitate_font_css(GUI.label_font())
 
-    protected var _name = text
-    protected var _start = int_to_pos(range.start)
-    protected var _end = int_to_pos(range.stop)
+    protected var _name: String = text
+    protected var _start: Position = int_to_pos(range.start)
+    protected var _end: Position = int_to_pos(range.stop)
     override def getIcon: Icon = null
     override def getShortString: String =
     {
@@ -84,7 +87,7 @@
   /* parsing */
 
   @volatile protected var stopped = false
-  override def stop() = { stopped = true }
+  override def stop(): Unit = { stopped = true }
 
   def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
 
@@ -229,7 +232,7 @@
     var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
     var start2: Option[(Int, String)] = None
 
-    def close1: Unit =
+    def close1(): Unit =
       start1 match {
         case Some((start_offset, s, body)) =>
           val node = make_node(s, start_offset, end_offset)
@@ -239,7 +242,7 @@
         case None =>
       }
 
-    def close2: Unit =
+    def close2(): Unit =
       start2 match {
         case Some((start_offset, s)) =>
           start1 match {
@@ -254,14 +257,14 @@
 
     for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
       line match {
-        case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
-        case Heading2(s) => close2; start2 = Some((offset, s))
+        case Heading1(s) => close2(); close1(); start1 = Some((offset, s, Vector()))
+        case Heading2(s) => close2(); start2 = Some((offset, s))
         case _ =>
       }
       offset += line.length + 1
       if (!line.forall(Character.isSpaceChar)) end_offset = offset
     }
-    if (!stopped) { close2; close1 }
+    if (!stopped) { close2(); close1() }
 
     true
   }
diff -r 57768f30d17c -r c13198575f75 src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Sat Jul 17 23:09:54 2021 +0200
@@ -74,7 +74,7 @@
       }
     }
     finally {
-      console_stream.flush
+      console_stream.flush()
       global_console = null
       global_out = null
       global_err = null
diff -r 57768f30d17c -r c13198575f75 src/Tools/jEdit/src/main.scala
--- a/src/Tools/jEdit/src/main.scala	Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Tools/jEdit/src/main.scala	Sat Jul 17 23:09:54 2021 +0200
@@ -104,7 +104,7 @@
             args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
               case Nil | List("--") =>
                 args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
-              case List(":") => args.slice(0, args.size - 1)
+              case List(":") => args.slice(0, args.length - 1)
               case _ => args
             }
           }
diff -r 57768f30d17c -r c13198575f75 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Sat Jul 17 23:09:54 2021 +0200
@@ -106,7 +106,7 @@
 
   /* theory files */
 
-  lazy val delay_init =
+  lazy val delay_init: Delay =
     Delay.last(options.seconds("editor_load_delay"), gui = true)
     {
       init_models()