# HG changeset patch
# User wenzelm
# Date 1668075446 -3600
# Node ID 08b950ca0313ee6ba97ecb42837a0c1577b22358
# Parent  1cebb0ca6d86902dd570b17e6836c1c329263ef9
tuned signature;

diff -r 1cebb0ca6d86 -r 08b950ca0313 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Nov 10 08:13:28 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Nov 10 11:17:26 2022 +0100
@@ -135,14 +135,14 @@
 
   object Selector {
     sealed abstract class Entry[A] {
-      def get_item: Option[A] =
+      def get_value: Option[A] =
         this match {
-          case item: Item[_] => Some(item.item)
+          case item: Item[_] => Some(item.value)
           case _ => None
         }
     }
-    case class Item[A](item: A, description: String = "", batch: Int = 0) extends Entry[A] {
-      override def toString: String = proper_string(description) getOrElse item.toString
+    case class Item[A](value: A, description: String = "", batch: Int = 0) extends Entry[A] {
+      override def toString: String = proper_string(description) getOrElse value.toString
     }
     case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
       override def toString: String = "<b>" + name + "</b>"
diff -r 1cebb0ca6d86 -r 08b950ca0313 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 10 08:13:28 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Nov 10 11:17:26 2022 +0100
@@ -91,7 +91,7 @@
       def load(): Unit = {
         val logic = options.string(jedit_logic_option)
         entries.find {
-          case item: GUI.Selector.Item[_] => item.item == logic
+          case item: GUI.Selector.Item[_] => item.value == logic
           case _ => false
         } match {
           case Some(entry) => selection.item = entry
@@ -99,7 +99,7 @@
         }
       }
       def save(): Unit =
-        for (item <- selection.item.get_item) options.string(jedit_logic_option) = item
+        for (item <- selection.item.get_value) options.string(jedit_logic_option) = item
 
       override def changed(): Unit = if (autosave) save()
 
diff -r 1cebb0ca6d86 -r 08b950ca0313 src/Tools/jEdit/src/jedit_spell_checker.scala
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Nov 10 08:13:28 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Thu Nov 10 11:17:26 2022 +0100
@@ -97,7 +97,7 @@
         }
       }
       def save(): Unit =
-        for (item <- selection.item.get_item) PIDE.options.string(option_name) = item.lang
+        for (item <- selection.item.get_value) PIDE.options.string(option_name) = item.lang
 
       load()
     }