# HG changeset patch # User wenzelm # Date 1668079304 -3600 # Node ID 15b058bb24161ded5c21cc7a925f2fa122888bf8 # Parent 5944f9e70d9833970d7ed9d738c76c4546085528 clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end; diff -r 5944f9e70d98 -r 15b058bb2416 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Nov 10 11:20:37 2022 +0100 +++ b/src/Pure/GUI/gui.scala Thu Nov 10 12:21:44 2022 +0100 @@ -134,28 +134,47 @@ /* list selector */ object Selector { - sealed abstract class Entry[A] { - def get_value: Option[A] = - this match { + object Value { + def unapply[A](entry: Entry[A]): Option[A] = + entry match { case item: Item[_] => Some(item.value) case _ => None } } - case class Item[A](value: A, description: String = "", batch: Int = 0) extends Entry[A] { + sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) } + private case class Item[A](value: A, description: String, batch: Int) extends Entry[A] { override def toString: String = proper_string(description) getOrElse value.toString } - case class Separator[A](batch: Int = 0) extends Entry[A] { + private case class Separator[A](batch: Int) extends Entry[A] { override def toString: String = "---" } - def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch) - def separator(batch: Int = 0): Separator[String] = Separator(batch = batch) + def item[A](value: A): Entry[A] = Item(value, "", 0) + def item_description[A](value: A, description: String): Entry[A] = Item(value, description, 0) + + def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = { + val item_batches: List[List[Item[A]]] = + batches.map(_.flatMap( + { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None })) + val sep_entries: List[Entry[A]] = + item_batches.filter(_.nonEmpty).zipWithIndex.flatMap({ case (batch, i) => + Separator[A](i) :: batch.map(_.copy(batch = i)) + }) + sep_entries.tail + } } - class Selector[A](val entries: List[Selector.Entry[A]]) - extends ComboBox[Selector.Entry[A]](entries) { + class Selector[A](batches: List[Selector.Entry[A]]*) + extends ComboBox[Selector.Entry[A]](Selector.make_entries(batches.toList)) { def changed(): Unit = {} + lazy val entries: List[Selector.Entry[A]] = Selector.make_entries(batches.toList) + + def find_value(pred: A => Boolean): Option[Selector.Entry[A]] = + entries.find({ case item: Selector.Item[A] => pred(item.value) case _ => false }) + + def selection_value: Option[A] = selection.item.get_value + override lazy val peer: JComboBox[Selector.Entry[A]] = new JComboBox[Selector.Entry[A]](ComboBox.newConstantModel(entries)) with SuperMixin { private var key_released = false @@ -206,7 +225,7 @@ class Zoom extends Selector[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%") - .map(GUI.Selector.item(_)) + .map(GUI.Selector.item) ) { def factor: Int = parse(selection.item.toString) @@ -228,7 +247,7 @@ } makeEditable()(c => - new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString)) + new ComboBox.BuiltInEditor(c)(text => Selector.item(print(parse(text))), _.toString)) peer.getEditor.getEditorComponent match { case text: JTextField => text.setColumns(4) case _ => diff -r 5944f9e70d98 -r 15b058bb2416 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Thu Nov 10 11:20:37 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Nov 10 12:21:44 2022 +0100 @@ -191,9 +191,9 @@ val sessions = JEdit_Sessions.sessions_structure() val all_sessions = sessions.build_topological_order.sorted val doc_sessions = all_sessions.filter(name => sessions(name).doc_group) - new GUI.Selector( - doc_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) ::: - all_sessions.map(GUI.Selector.item(_, batch = 1)) + new GUI.Selector[String]( + doc_sessions.map(GUI.Selector.item), + all_sessions.map(GUI.Selector.item) ) { val title = "Session" } diff -r 5944f9e70d98 -r 15b058bb2416 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 10 11:20:37 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 10 12:21:44 2022 +0100 @@ -72,34 +72,26 @@ def logic_selector(options: Options_Variable, autosave: Boolean = false): JEdit_Options.Entry = { GUI_Thread.require {} - val default_entry = - GUI.Selector.Item("", description = "default (" + logic_name(options.value) + ")") + val sessions = sessions_structure(options = options.value) + val all_sessions = sessions.imports_topological_order + val main_sessions = all_sessions.filter(name => sessions(name).main_group) - val session_entries = { - val sessions = sessions_structure(options = options.value) - val all_sessions = sessions.imports_topological_order - val main_sessions = all_sessions.filter(name => sessions(name).main_group) + val default_entry = + GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")") - main_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) ::: - all_sessions.sorted.map(GUI.Selector.item(_, batch = 1)) - } - - new GUI.Selector(default_entry :: session_entries) with JEdit_Options.Entry { + new GUI.Selector[String]( + default_entry :: main_sessions.map(GUI.Selector.item), + all_sessions.sorted.map(GUI.Selector.item) + ) with JEdit_Options.Entry { name = jedit_logic_option tooltip = "Logic session name (change requires restart)" val title = "Logic" def load(): Unit = { val logic = options.string(jedit_logic_option) - entries.find { - case item: GUI.Selector.Item[_] => item.value == logic - case _ => false - } match { - case Some(entry) => selection.item = entry - case None => - } + for (entry <- find_value(_ == logic)) selection.item = entry } def save(): Unit = - for (item <- selection.item.get_value) options.string(jedit_logic_option) = item + for (logic <- selection_value) options.string(jedit_logic_option) = logic override def changed(): Unit = if (autosave) save() diff -r 5944f9e70d98 -r 15b058bb2416 src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Nov 10 11:20:37 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Nov 10 12:21:44 2022 +0100 @@ -85,19 +85,19 @@ val option_name = "spell_checker_dictionary" val opt = PIDE.options.value.check_name(option_name) - new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.Item(_))) with JEdit_Options.Entry { + new GUI.Selector(Spell_Checker.dictionaries.map(GUI.Selector.item)) with JEdit_Options.Entry { name = option_name tooltip = GUI.tooltip_lines(opt.print_default) val title = opt.title() def load(): Unit = { val lang = PIDE.options.string(option_name) Spell_Checker.get_dictionary(lang) match { - case Some(dict) => selection.item = GUI.Selector.Item(dict) + case Some(dict) => selection.item = GUI.Selector.item(dict) case None => } } def save(): Unit = - for (item <- selection.item.get_value) PIDE.options.string(option_name) = item.lang + for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang load() }