--- 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>"
--- 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()
--- 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()
}