# HG changeset patch
# User wenzelm
# Date 1733569191 -3600
# Node ID a296642fa0a5b03ad17545d3438dbe0039e7f8cd
# Parent  2f43a87a7d0628454501a8e3a2496e61f4add7b8
clarified GUI: prefer user documents, which are typically without chapter;

diff -r 2f43a87a7d06 -r a296642fa0a5 src/Pure/Build/sessions.scala
--- 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")
 
diff -r 2f43a87a7d06 -r a296642fa0a5 src/Tools/jEdit/src/jedit_sessions.scala
--- 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:_*)
     }