clarified modules;
authorwenzelm
Mon Apr 24 11:05:24 2017 +0200 (2017-04-24)
changeset 65571923e32ad0976
parent 65570 660df4a6dc59
child 65572 6acb28e5ba41
clarified modules;
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Apr 23 23:54:06 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Mon Apr 24 11:05:24 2017 +0200
     1.3 @@ -49,6 +49,11 @@
     1.4  
     1.5    def session_name(options: Options): String = session_info(options).name
     1.6  
     1.7 +  def session_base(options: Options): Sessions.Base =
     1.8 +    Sessions.session_base(
     1.9 +      options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
    1.10 +    .platform_path
    1.11 +
    1.12    def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    1.13  
    1.14    def session_build(
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 23:54:06 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 24 11:05:24 2017 +0200
     2.3 @@ -68,16 +68,8 @@
     2.4    /* resources */
     2.5  
     2.6    private var _resources: JEdit_Resources = null
     2.7 -  private def init_resources()
     2.8 -  {
     2.9 -    val options = this.options.value
    2.10 -    val session_name = JEdit_Sessions.session_name(options)
    2.11 -    val session_base =
    2.12 -      Sessions.session_base(
    2.13 -        options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
    2.14 -
    2.15 -    _resources = new JEdit_Resources(session_base.platform_path)
    2.16 -  }
    2.17 +  private def init_resources(): Unit =
    2.18 +    _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
    2.19    def resources: JEdit_Resources = _resources
    2.20  
    2.21