# 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 =>