# 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 = "<b>" + name + "</b>"
+    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()
     }