# HG changeset patch
# User wenzelm
# Date 1671724464 -3600
# Node ID 3f41f3c3696c34d1c56d9af29f5dabe79fd034de
# Parent  ec07b1af45c555d3063a81a39937b5a346fe6ef5
only show sessions with document setup;

diff -r ec07b1af45c5 -r 3f41f3c3696c src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu Dec 22 16:53:45 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Dec 22 16:54:24 2022 +0100
@@ -113,8 +113,9 @@
 
   def document_selector(options: Options_Variable, standalone: Boolean = false): Selector =
     GUI_Thread.require {
-      val sessions = sessions_structure(options = options.value)
-      val all_sessions = sessions.build_topological_order.sorted
+      val sessions = sessions_structure(options = options.value + "document")
+      val all_sessions =
+        sessions.build_topological_order.filter(name => sessions(name).documents.nonEmpty).sorted
       val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
 
       new Selector(options, "editor_document_session", standalone,