# HG changeset patch
# User wenzelm
# Date 1668075637 -3600
# Node ID 5944f9e70d9833970d7ed9d738c76c4546085528
# Parent  08b950ca0313ee6ba97ecb42837a0c1577b22358
clarified signature: only support nameless separator;

diff -r 08b950ca0313 -r 5944f9e70d98 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Nov 10 11:17:26 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Nov 10 11:20:37 2022 +0100
@@ -144,8 +144,8 @@
     case class Item[A](value: A, description: String = "", batch: Int = 0) 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>"
+    case class Separator[A](batch: Int = 0) extends Entry[A] {
+      override def toString: String = "---"
     }
 
     def item(name: String, batch: Int = 0): Item[String] = Item(name, batch = batch)
@@ -187,13 +187,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)
         }
       }