src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Wed Nov 09 20:30:52 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 09 21:14:20 2022 +0100
@@ -9,10 +9,11 @@
 import java.util.{Map => JMap}
 import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
   Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
+import java.awt.event.{KeyAdapter, KeyEvent, ItemListener, ItemEvent}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
-  JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
+  JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities}
 
 import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
   Orientation}
@@ -136,25 +137,54 @@
     sealed abstract class Entry[A] {
       def get_item: Option[A] =
         this match {
-          case Item(item, _) => Some(item)
+          case item: Item[_] => Some(item.item)
           case _ => None
         }
     }
-    case class Item[A](item: A, description: String = "") extends Entry[A] {
+    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 Separator[A](name: String = "") extends Entry[A] {
+    case class Separator[A](name: String = "", batch: Int = 0) extends Entry[A] {
       override def toString: String = "<b>" + name + "</b>"
     }
 
-    def item(name: String): Item[String] = Item(name)
-    def separator: Separator[String] = Separator()
+    def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
+    def separator(batch: Int = 0): Separator[String] = Separator(batch = batch)
   }
 
   class Selector[A](val entries: List[Selector.Entry[A]])
   extends ComboBox[Selector.Entry[A]](entries) {
     def changed(): Unit = {}
 
+    override lazy val peer: JComboBox[Selector.Entry[A]] =
+      new JComboBox[Selector.Entry[A]](ComboBox.newConstantModel(entries)) with SuperMixin {
+        private var key_released = false
+        private var sep_selected = false
+
+        addKeyListener(new KeyAdapter {
+          override def keyPressed(e: KeyEvent): Unit = { key_released = false }
+          override def keyReleased(e: KeyEvent): Unit = { key_released = true }
+        })
+
+        override def setSelectedIndex(i: Int): Unit = {
+          getItemAt(i) match {
+            case _: Selector.Separator[_] =>
+              if (key_released) { sep_selected = true }
+              else {
+                val k = getSelectedIndex()
+                val j = if (i > k) i + 1 else i - 1
+                if (0 <= j && j < dataModel.getSize()) super.setSelectedIndex(j)
+              }
+            case _ => super.setSelectedIndex(i)
+          }
+        }
+
+        override def setPopupVisible(visible: Boolean): Unit = {
+          if (sep_selected) { sep_selected = false}
+          else super.setPopupVisible(visible)
+        }
+      }
+
     private val default_renderer = renderer
     private val render_separator = new Separator
     private val render_label = new Label
@@ -179,7 +209,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)