src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Wed Nov 09 14:20:52 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 09 19:42:21 2022 +0100
@@ -13,7 +13,9 @@
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane,
   JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities}
-import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea}
+
+import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator,
+  Orientation}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 
@@ -127,9 +129,45 @@
     reactions += { case ButtonClicked(_) => clicked(selected); clicked() }
   }
 
-  class Selector[A](val entries: List[A]) extends ComboBox[A](entries) {
+
+  /* list selector */
+
+  object Selector {
+    sealed abstract class Entry[A] {
+      def get_item: Option[A] =
+        this match {
+          case Item(item, _) => Some(item)
+          case _ => None
+        }
+    }
+    case class Item[A](item: A, description: String = "") extends Entry[A] {
+      override def toString: String = proper_string(description) getOrElse item.toString
+    }
+    case class Separator[A](name: String = "") extends Entry[A] {
+      override def toString: String = "<b>" + name + "</b>"
+    }
+
+    def item(name: String): Item[String] = Item(name)
+    def separator: Separator[String] = Separator()
+  }
+
+  class Selector[A](val entries: List[Selector.Entry[A]])
+  extends ComboBox[Selector.Entry[A]](entries) {
     def changed(): Unit = {}
 
+    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 _ => default_renderer.componentFor(list, selected, focus, entry, i)
+        }
+      }
+
     listenTo(selection)
     reactions += { case SelectionChanged(_) => changed() }
   }
@@ -141,8 +179,9 @@
 
   class Zoom extends Selector[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
+      .map(GUI.Selector.item)
   ) {
-    def factor: Int = parse(selection.item)
+    def factor: Int = parse(selection.item.toString)
 
     private def parse(text: String): Int =
       text match {
@@ -161,7 +200,8 @@
       }
     }
 
-    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+    makeEditable()(c =>
+      new ComboBox.BuiltInEditor(c)(text => Selector.Item(print(parse(text))), _.toString))
     peer.getEditor.getEditorComponent match {
       case text: JTextField => text.setColumns(4)
       case _ =>