# HG changeset patch # User wenzelm # Date 1668088520 -3600 # Node ID ac5833ebe6d16bc31e14d0af82901d799d3428f2 # Parent 7956b822f2392bc1b0cd670d9e03daa20cdb1a3f# Parent e0d79728363834383da38d6aed7530cfa44db0f2 merged diff -r 7956b822f239 -r ac5833ebe6d1 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Nov 10 11:49:34 2022 +0100 +++ b/src/Pure/GUI/gui.scala Thu Nov 10 14:55:20 2022 +0100 @@ -134,28 +134,47 @@ /* list selector */ object Selector { - sealed abstract class Entry[A] { - def get_item: Option[A] = - this match { - case item: Item[_] => Some(item.item) + sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) } + object Value { + def unapply[A](entry: Entry[A]): Option[A] = + entry match { + 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 + def item[A](value: A): Entry[A] = Item(value, "", 0) + def item_description[A](value: A, description: String): Entry[A] = Item(value, description, 0) + + 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](name: String = "", batch: Int = 0) extends Entry[A] { - override def toString: String = "" + name + "" + 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) + private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = { + val item_batches = + 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 @@ -187,13 +206,10 @@ private val default_renderer = renderer private val render_separator = new Separator - private val render_label = new Label renderer = (list: ListView[_ <: Selector.Entry[A]], selected: Boolean, focus: Boolean, entry: Selector.Entry[A], i: Int) => { entry match { - case sep: Selector.Separator[_] => - if (sep.name.isEmpty) render_separator - else { render_label.text = entry.toString; render_label } + case _: Selector.Separator[_] => render_separator case _ => default_renderer.componentFor(list, selected, focus, entry, i) } } @@ -209,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) @@ -231,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 7956b822f239 -r ac5833ebe6d1 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Thu Nov 10 11:49:34 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Nov 10 14:55:20 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 7956b822f239 -r ac5833ebe6d1 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 10 11:49:34 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Nov 10 14:55:20 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.item == 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_item) 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 7956b822f239 -r ac5833ebe6d1 src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Nov 10 11:49:34 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Thu Nov 10 14:55:20 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_item) PIDE.options.string(option_name) = item.lang + for (dict <- selection_value) PIDE.options.string(option_name) = dict.lang load() }