# HG changeset patch
# User wenzelm
# Date 1668024860 -3600
# Node ID 9686049ce9889da6bf43dbc0ac65bf621d8fdcfb
# Parent  2dfc8885c0ee21cb5ce42f5839febb942dd3aac3
more robust selection: avoid duplicates via "batch" number;
evade attempts to select separator via keyboard or mouse (non-keyboard), assuming there are no consecutive separators;

diff -r 2dfc8885c0ee -r 9686049ce988 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)
 
diff -r 2dfc8885c0ee -r 9686049ce988 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 20:30:52 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 21:14:20 2022 +0100
@@ -192,8 +192,8 @@
     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)
+      doc_sessions.map(GUI.Selector.item(_)) ::: List(GUI.Selector.separator()) :::
+      all_sessions.map(GUI.Selector.item(_, batch = 1))
     ) {
       val title = "Session"
     }
diff -r 2dfc8885c0ee -r 9686049ce988 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 20:30:52 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 09 21:14:20 2022 +0100
@@ -80,8 +80,8 @@
       val all_sessions = sessions.imports_topological_order
       val main_sessions = all_sessions.filter(name => sessions(name).main_group)
 
-      main_sessions.map(GUI.Selector.item) ::: List(GUI.Selector.separator) :::
-      all_sessions.sorted.map(GUI.Selector.item)
+      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 {
@@ -90,7 +90,10 @@
       val title = "Logic"
       def load(): Unit = {
         val logic = options.string(jedit_logic_option)
-        entries.find { case GUI.Selector.Item(item, _) => item == logic case _ => false } match {
+        entries.find {
+          case item: GUI.Selector.Item[_] => item.item == logic
+          case _ => false
+        } match {
           case Some(entry) => selection.item = entry
           case None =>
         }