# HG changeset patch
# User wenzelm
# Date 1660302962 -7200
# Node ID b702a015fb22bdcb9144470958e3896710c164b8
# Parent  91f02f224b8090fe6e0726a965b13e56c1b76227
clarified signature;

diff -r 91f02f224b80 -r b702a015fb22 src/Tools/jEdit/src/isabelle_session.scala
--- 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 {
diff -r 91f02f224b80 -r b702a015fb22 src/Tools/jEdit/src/jedit_sessions.scala
--- 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