--- a/src/Pure/Build/sessions.scala Sat Dec 07 11:13:02 2024 +0100
+++ b/src/Pure/Build/sessions.scala Sat Dec 07 11:59:51 2024 +0100
@@ -709,6 +709,8 @@
def dirs: List[Path] = dir :: directories
+ def unsorted_chapter: Boolean = chapter == UNSORTED
+
def main_group: Boolean = groups.contains("main")
def doc_group: Boolean = groups.contains("doc")
--- a/src/Tools/jEdit/src/jedit_sessions.scala Sat Dec 07 11:13:02 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sat Dec 07 11:59:51 2024 +0100
@@ -130,10 +130,12 @@
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)
+ val unsorted_sessions = all_sessions.filter(name => sessions(name).unsorted_chapter)
- new Selector(options, "editor_document_session", standalone,
- doc_sessions.map(GUI.Selector.item),
- all_sessions.map(GUI.Selector.item))
+ val batches =
+ (if (unsorted_sessions.nonEmpty) List(unsorted_sessions.map(GUI.Selector.item)) else Nil) :::
+ List(doc_sessions.map(GUI.Selector.item), all_sessions.map(GUI.Selector.item))
+ new Selector(options, "editor_document_session", standalone, batches:_*)
}