# HG changeset patch
# User wenzelm
# Date 1660326458 -7200
# Node ID 4920ebbde4869b68b3492cfb94b967f2d5cd805c
# Parent  d298da61655af5151de6cac07ff680037eaaf9cb
tuned, following hints by IntelliJ IDEA;

diff -r d298da61655a -r 4920ebbde486 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Aug 12 16:58:30 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Aug 12 19:47:38 2022 +0200
@@ -57,9 +57,9 @@
 
     val button = new ColorWellButton(Color_Value(opt.value))
     val component = new Component with Option_Component {
-      override lazy val peer = button
+      override lazy val peer: JComponent = button
       name = opt_name
-      val title = opt_title
+      val title: String = opt_title
       def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
       def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
     }
@@ -77,7 +77,7 @@
       if (opt.typ == Options.Bool)
         new CheckBox with Option_Component {
           name = opt_name
-          val title = opt_title
+          val title: String = opt_title
           def load(): Unit = selected = bool(opt_name)
           def save(): Unit = bool(opt_name) = selected
         }
@@ -87,7 +87,7 @@
           new TextArea with Option_Component {
             if (default_font != null) font = default_font
             name = opt_name
-            val title = opt_title
+            val title: String = opt_title
             def load(): Unit = text = value.check_name(opt_name).value
             def save(): Unit =
               try { JEdit_Options.this += (opt_name, text) }
@@ -97,14 +97,11 @@
                     GUI.scrollable_text(msg))
               }
           }
-        text_area.peer.setInputVerifier(new InputVerifier {
-          def verify(jcomponent: JComponent): Boolean =
-            jcomponent match {
-              case text: JTextComponent =>
-                try { value + (opt_name, text.getText); true }
-                catch { case ERROR(_) => false }
-              case _ => true
-            }
+        text_area.peer.setInputVerifier({
+            case text: JTextComponent =>
+              try { value + (opt_name, text.getText); true }
+              catch { case ERROR(_) => false }
+            case _ => true
           })
         GUI.plain_focus_traversal(text_area.peer)
         text_area