tuned signature;

--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 15:59:06 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 16:14:14 2022 +0200
@@ -19,12 +19,6 @@
 import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
 
 
-trait Option_Component extends Component {
-  val title: String
-  def load(): Unit
-  def save(): Unit
-}
-
 object JEdit_Options {
   /* sections */
 
@@ -86,8 +80,14 @@
 
   /* editor pane for plugin options */
 
+  trait Entry extends Component {
+    val title: String
+    def load(): Unit
+    def save(): Unit
+  }
+
   abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
-    protected val components: List[(String, List[Option_Component])]
+    protected val components: List[(String, List[Entry])]
 
     override def _init(): Unit = {
       val dummy_property = "options.isabelle.dummy"
@@ -115,7 +115,7 @@
       List(JEdit_Sessions.logic_selector(options),
         JEdit_Spell_Checker.dictionaries_selector())
 
-    protected val components: List[(String, List[Option_Component])] =
+    protected val components: List[(String, List[Entry])] =
       options.make_components(predefined,
         (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
   }
@@ -130,7 +130,7 @@
 
     assert(predefined.nonEmpty)
 
-    protected val components: List[(String, List[Option_Component])] =
+    protected val components: List[(String, List[Entry])] =
       PIDE.options.make_components(predefined, _ => false)
   }
 }
@@ -138,25 +138,26 @@
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
   def color_value(s: String): Color = Color_Value(string(s))
 
-  def make_color_component(opt: Options.Opt): Option_Component = {
+  def make_color_component(opt: Options.Opt): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
 
     val button = new ColorWellButton(Color_Value(opt.value))
-    val component = new Component with Option_Component {
-      override lazy val peer: JComponent = button
-      name = opt_name
-      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)
-    }
+    val component =
+      new Component with JEdit_Options.Entry {
+        override lazy val peer: JComponent = button
+        name = opt_name
+        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)
+      }
     component.tooltip = GUI.tooltip_lines(opt.print_default)
     component
   }
 
-  def make_component(opt: Options.Opt): Option_Component = {
+  def make_component(opt: Options.Opt): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val opt_name = opt.name
@@ -164,7 +165,7 @@
 
     val component =
       if (opt.typ == Options.Bool)
-        new CheckBox with Option_Component {
+        new CheckBox with JEdit_Options.Entry {
           name = opt_name
           val title: String = opt_title
           def load(): Unit = selected = bool(opt_name)
@@ -173,7 +174,7 @@
       else {
         val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
         val text_area =
-          new TextArea with Option_Component {
+          new TextArea with JEdit_Options.Entry {
             if (default_font != null) font = default_font
             name = opt_name
             val title: String = opt_title
@@ -201,10 +202,10 @@
   }
 
   def make_components(
-    predefined: List[Option_Component],
+    predefined: List[JEdit_Options.Entry],
     filter: String => Boolean
-  ) : List[(String, List[Option_Component])] = {
-    def mk_component(opt: Options.Opt): List[Option_Component] =
+  ) : List[(String, List[JEdit_Options.Entry])] = {
+    def mk_component(opt: Options.Opt): List[JEdit_Options.Entry] =
       predefined.find(opt.name == _.name) match {
         case Some(c) => List(c)
         case None => if (filter(opt.name)) List(make_component(opt)) else Nil

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Oct 28 15:59:06 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Oct 28 16:14:14 2022 +0200
@@ -73,7 +73,7 @@
     override def toString: String = proper_string(description) getOrElse name
   }
 
-  def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = {
+  def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")")
@@ -85,7 +85,8 @@
       (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name))
     }
 
-    new GUI.Selector[Logic_Entry](default_entry :: session_entries) with Option_Component {
+    new GUI.Selector[Logic_Entry](default_entry :: session_entries)
+    with JEdit_Options.Entry {
       name = jedit_logic_option
       tooltip = "Logic session name (change requires restart)"
       val title = "Logic"

--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Oct 28 15:59:06 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Fri Oct 28 16:14:14 2022 +0200
@@ -79,13 +79,13 @@
 
   /* dictionaries */
 
-  def dictionaries_selector(): Option_Component = {
+  def dictionaries_selector(): JEdit_Options.Entry = {
     GUI_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
 
-    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component {
+    new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with JEdit_Options.Entry {
       name = option_name
       tooltip = GUI.tooltip_lines(opt.print_default)
       val title = opt.title()