--- a/src/Tools/jEdit/src/isabelle_session.scala Fri Aug 12 12:50:19 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala Fri Aug 12 13:16:02 2022 +0200
@@ -18,12 +18,6 @@
object Isabelle_Session {
- /* sessions structure */
-
- def sessions_structure(): Sessions.Structure =
- JEdit_Sessions.sessions_structure(PIDE.options.value)
-
-
/* virtual file-system */
val vfs_prefix = "isabelle-session:"
@@ -53,7 +47,7 @@
explode_url(url, component = component) match {
case None => null
case Some(elems) =>
- val sessions = sessions_structure()
+ val sessions = JEdit_Sessions.sessions_structure()
elems match {
case Nil =>
sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray
@@ -90,7 +84,7 @@
PIDE.maybe_snapshot(view) match {
case None => ""
case Some(snapshot) =>
- val sessions = sessions_structure()
+ val sessions = JEdit_Sessions.sessions_structure()
val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
val chapter =
sessions.get(session) match {
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 12:50:19 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 13:16:02 2022 +0200
@@ -39,8 +39,12 @@
options2
}
- def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure =
+ def sessions_structure(
+ options: Options = PIDE.options.value,
+ dirs: List[Path] = session_dirs
+ ): Sessions.Structure = {
Sessions.load_structure(session_options(options), dirs = dirs)
+ }
/* raw logic info */
@@ -58,7 +62,7 @@
space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
- try { sessions_structure(options).get(logic_name(options)) }
+ try { sessions_structure(options = options).get(logic_name(options)) }
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
@@ -76,7 +80,7 @@
GUI_Thread.require {}
val session_list = {
- val sessions = sessions_structure(options.value)
+ val sessions = sessions_structure(options = options.value)
val (main_sessions, other_sessions) =
sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
main_sessions.sorted ::: other_sessions.sorted