tuned signature;

--- a/src/Pure/GUI/gui.scala	Thu Nov 10 12:21:44 2022 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Nov 10 12:25:28 2022 +0100
@@ -134,6 +134,7 @@
   /* list selector */
 
   object Selector {
+    sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) }
     object Value {
       def unapply[A](entry: Entry[A]): Option[A] =
         entry match {
@@ -141,7 +142,9 @@
           case _ => None
         }
     }
-    sealed abstract class Entry[A] { def get_value: Option[A] = Value.unapply(this) }
+    def item[A](value: A): Entry[A] = Item(value, "", 0)
+    def item_description[A](value: A, description: String): Entry[A] = Item(value, description, 0)
+
     private case class Item[A](value: A, description: String, batch: Int) extends Entry[A] {
       override def toString: String = proper_string(description) getOrElse value.toString
     }
@@ -149,11 +152,8 @@
       override def toString: String = "---"
     }
 
-    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]]] =
+    private def make_entries[A](batches: List[List[Entry[A]]]): List[Entry[A]] = {
+      val item_batches =
         batches.map(_.flatMap(
           { case item: Item[_] => Some(item.asInstanceOf[Item[A]]) case _ => None }))
       val sep_entries: List[Entry[A]] =