src/Tools/jEdit/src/plugin.scala
changeset 65571 923e32ad0976
parent 65554 a04afc400156
child 66019 69b5ef78fb07
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 23:54:06 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 24 11:05:24 2017 +0200
     1.3 @@ -68,16 +68,8 @@
     1.4    /* resources */
     1.5  
     1.6    private var _resources: JEdit_Resources = null
     1.7 -  private def init_resources()
     1.8 -  {
     1.9 -    val options = this.options.value
    1.10 -    val session_name = JEdit_Sessions.session_name(options)
    1.11 -    val session_base =
    1.12 -      Sessions.session_base(
    1.13 -        options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
    1.14 -
    1.15 -    _resources = new JEdit_Resources(session_base.platform_path)
    1.16 -  }
    1.17 +  private def init_resources(): Unit =
    1.18 +    _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
    1.19    def resources: JEdit_Resources = _resources
    1.20  
    1.21