# HG changeset patch
# User wenzelm
# Date 1548858319 -3600
# Node ID 34a93af5b96938de684dec1d5c582d0b18a5930d
# Parent  da0d533d7f309ed5137fd69f9349b4fd1470bb97
tuned signature;

diff -r da0d533d7f30 -r 34a93af5b969 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Jan 30 14:40:23 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Jan 30 15:25:19 2019 +0100
@@ -29,6 +29,9 @@
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
+  def sessions_structure(options: Options, dirs: List[Path] = session_dirs()): Sessions.Structure =
+    Sessions.load_structure(session_options(options), dirs = dirs)
+
 
   /* raw logic info */
 
@@ -46,10 +49,7 @@
     space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
 
   def logic_info(options: Options): Option[Sessions.Info] =
-    try {
-      Sessions.load_structure(session_options(options), dirs = session_dirs()).
-        get(logic_name(options))
-    }
+    try { sessions_structure(options).get(logic_name(options)) }
     catch { case ERROR(_) => None }
 
   def logic_root(options: Options): Position.T =
@@ -70,10 +70,9 @@
 
     val session_list =
     {
-      val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
+      val sessions = sessions_structure(options.value)
       val (main_sessions, other_sessions) =
-        sessions_structure.imports_topological_order.
-          partition(name => sessions_structure(name).groups.contains("main"))
+        sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main"))
       main_sessions.sorted ::: other_sessions.sorted
     }