proper session chapter;
authorwenzelm
Thu May 09 14:50:56 2019 +0200 (6 months ago)
changeset 70253cb334a92a4db
parent 70252 236c1bb128da
child 70254 5a00e8624488
proper session chapter;
cannot access session: refers to ROOT entry;
src/Tools/jEdit/src/isabelle_session.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle_session.scala	Thu May 09 14:22:25 2019 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_session.scala	Thu May 09 14:50:56 2019 +0200
     1.3 @@ -88,8 +88,12 @@
     1.4          case Some(snapshot) =>
     1.5            val sessions = sessions_structure()
     1.6            val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
     1.7 -          val chapter = sessions.get(session).getOrElse(Sessions.UNSORTED)
     1.8 -          chapter + "/" + session
     1.9 +          val chapter =
    1.10 +            sessions.get(session) match {
    1.11 +              case Some(info) => info.chapter
    1.12 +              case None => Sessions.UNSORTED
    1.13 +            }
    1.14 +          chapter
    1.15        }
    1.16      VFSBrowser.browseDirectory(view, vfs_prefix + path)
    1.17    }