--- 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)