# HG changeset patch
# User wenzelm
# Date 1670334073 -3600
# Node ID c662a56e77a87f54b1001dd3b263972a99309191
# Parent  6714991edf8b6b6ca5b5ee8e0699fd53e9d05494
tuned;

diff -r 6714991edf8b -r c662a56e77a8 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 06 08:50:57 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 06 14:41:13 2022 +0100
@@ -193,14 +193,11 @@
 
   private val document_session: GUI.Selector[String] = {
     val sessions = JEdit_Sessions.sessions_structure()
-    val all_sessions = sessions.build_topological_order.sorted
-    val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
-    new GUI.Selector[String](
-      doc_sessions.map(GUI.Selector.item),
-      all_sessions.map(GUI.Selector.item)
-    ) {
-      val title = "Session"
-    }
+    val all_sessions = sessions.build_topological_order.sorted.map(GUI.Selector.item)
+    val doc_sessions =
+      for (entry <- all_sessions; name <- entry.get_value if sessions(name).doc_group)
+        yield entry
+    new GUI.Selector[String](doc_sessions, all_sessions) { val title = "Session" }
   }
 
   private val build_button =
diff -r 6714991edf8b -r c662a56e77a8 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Tue Dec 06 08:50:57 2022 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Tue Dec 06 14:41:13 2022 +0100
@@ -65,7 +65,7 @@
   /* controls */
 
   private val select_data =
-    new GUI.Selector(ML_Statistics.all_fields.map { case (a, _) => GUI.Selector.item(a) }) {
+    new GUI.Selector(ML_Statistics.all_fields.map(p => GUI.Selector.item(p._1))) {
       tooltip = "Select visualized data collection"
       override def changed(): Unit = { data_name = selection.item.toString; update_chart() }
     }