# HG changeset patch
# User wenzelm
# Date 1493024724 -7200
# Node ID 923e32ad09764b582ecfc1bd28243476bfaa3aef
# Parent  660df4a6dc59988061497751c6825267512ceebd
clarified modules;

diff -r 660df4a6dc59 -r 923e32ad0976 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Apr 23 23:54:06 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:05:24 2017 +0200
@@ -49,6 +49,11 @@
 
   def session_name(options: Options): String = session_info(options).name
 
+  def session_base(options: Options): Sessions.Base =
+    Sessions.session_base(
+      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
+    .platform_path
+
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
 
   def session_build(
diff -r 660df4a6dc59 -r 923e32ad0976 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 23:54:06 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 24 11:05:24 2017 +0200
@@ -68,16 +68,8 @@
   /* resources */
 
   private var _resources: JEdit_Resources = null
-  private def init_resources()
-  {
-    val options = this.options.value
-    val session_name = JEdit_Sessions.session_name(options)
-    val session_base =
-      Sessions.session_base(
-        options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
-
-    _resources = new JEdit_Resources(session_base.platform_path)
-  }
+  private def init_resources(): Unit =
+    _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
   def resources: JEdit_Resources = _resources