--- 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"
}