clarified modules;
authorwenzelm
Mon, 24 Apr 2017 11:05:24 +0200
changeset 65571 923e32ad0976
parent 65570 660df4a6dc59
child 65572 6acb28e5ba41
clarified modules;
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.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(
--- 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