# HG changeset patch
# User wenzelm
# Date 1670340419 -3600
# Node ID c79b43c1c7abb5c3938b6f60343c37ba8d24e2da
# Parent  06b001094ddb421a6be4582edff198944fb5b12a
tuned signature;

diff -r 06b001094ddb -r c79b43c1c7ab src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Dec 06 16:23:49 2022 +0100
+++ b/src/Pure/System/options.scala	Tue Dec 06 16:26:59 2022 +0100
@@ -79,6 +79,7 @@
         }
       Word.implode(words1.map(Word.perhaps_capitalize))
     }
+    def title_jedit: String = title("jedit")
 
     def unknown: Boolean = typ == Unknown
   }
diff -r 06b001094ddb -r c79b43c1c7ab src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Tue Dec 06 16:23:49 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Dec 06 16:26:59 2022 +0100
@@ -137,7 +137,7 @@
     GUI_Thread.require {}
 
     val opt_name = opt.name
-    val opt_title = opt.title("jedit")
+    val opt_title = opt.title_jedit
 
     val button = new ColorWellButton(Color_Value(opt.value))
     val component =
@@ -156,7 +156,7 @@
     GUI_Thread.require {}
 
     val opt_name = opt.name
-    val opt_title = opt.title("jedit")
+    val opt_title = opt.title_jedit
 
     val component =
       if (opt.typ == Options.Bool)
@@ -206,7 +206,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 06b001094ddb -r c79b43c1c7ab src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:23:49 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:26:59 2022 +0100
@@ -79,7 +79,7 @@
     tooltip = Word.capitalize(options.value.description(option_name))
 
     override val title: String =
-      options.value.check_name(option_name).title("jedit")
+      options.value.check_name(option_name).title_jedit
     override def load(): Unit = {
       val value = options.string(option_name)
       for (entry <- find_value(_ == value)) selection.item = entry