--- 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