# HG changeset patch
# User wenzelm
# Date 1661609281 -7200
# Node ID 64b05dc566563253227bcb9cf49ab7726c2180ae
# Parent  7032b0886f9a291ff06a3c03a929e18098f78253
tuned signature;

diff -r 7032b0886f9a -r 64b05dc56656 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 15:44:51 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 16:08:01 2022 +0200
@@ -762,7 +762,7 @@
       chapters1 ::: chapters2
     }
 
-    def chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty)
+    def relevant_chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty)
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
diff -r 7032b0886f9a -r 64b05dc56656 src/Tools/jEdit/src/isabelle_session.scala
--- a/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 15:44:51 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 16:08:01 2022 +0200
@@ -50,9 +50,9 @@
           val sessions = JEdit_Sessions.sessions_structure()
           elems match {
             case Nil =>
-              sessions.chapters.sortBy(_.name).map(ch => make_entry(ch.name, is_dir = true)).toArray
+              sessions.relevant_chapters.sortBy(_.name).map(ch => make_entry(ch.name, is_dir = true)).toArray
             case List(chapter) =>
-              sessions.chapters.find(_.name == chapter) match {
+              sessions.relevant_chapters.find(_.name == chapter) match {
                 case None => null
                 case Some(chapter_info) =>
                   chapter_info.sessions.map { session =>