clarified GUI: prefer user documents, which are typically without chapter;
authorwenzelm
Sat, 07 Dec 2024 11:59:51 +0100
changeset 81551 a296642fa0a5
parent 81550 2f43a87a7d06
child 81552 4717d3bf5752
clarified GUI: prefer user documents, which are typically without chapter;
src/Pure/Build/sessions.scala
src/Tools/jEdit/src/jedit_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")
 
--- 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:_*)
     }