equal
deleted
inserted
replaced
26 def apply(options: Options): JEdit_Resources = |
26 def apply(options: Options): JEdit_Resources = |
27 new JEdit_Resources(JEdit_Sessions.session_base_info(options)) |
27 new JEdit_Resources(JEdit_Sessions.session_base_info(options)) |
28 } |
28 } |
29 |
29 |
30 class JEdit_Resources private(session_base_info: Sessions.Base_Info) |
30 class JEdit_Resources private(session_base_info: Sessions.Base_Info) |
31 extends Resources(session_base_info.base) |
31 extends Resources(session_base_info.base.platform_path) |
32 { |
32 { |
33 def session_errors: List[String] = session_base_info.errors |
33 def session_errors: List[String] = session_base_info.errors |
34 |
34 |
35 |
35 |
36 /* document node name */ |
36 /* document node name */ |