# HG changeset patch
# User wenzelm
# Date 1661610837 -7200
# Node ID a84e9594ec7eb6e27a502b92ec666d6f4e73b595
# Parent  64b05dc566563253227bcb9cf49ab7726c2180ae
tuned;

diff -r 64b05dc56656 -r a84e9594ec7e src/Tools/jEdit/src/isabelle_session.scala
--- a/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 16:08:01 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 16:33:57 2022 +0200
@@ -54,10 +54,10 @@
             case List(chapter) =>
               sessions.relevant_chapters.find(_.name == chapter) match {
                 case None => null
-                case Some(chapter_info) =>
-                  chapter_info.sessions.map { session =>
+                case Some(ch) =>
+                  ch.sessions.map { session =>
                     val pos = sessions(session).pos
-                    val name = chapter_info.name + "/" + session
+                    val name = ch.name + "/" + session
                     val path =
                       Position.File.unapply(pos) match {
                         case Some(path) => File.platform_path(path)