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 _ =>