equal
deleted
inserted
replaced
22 |
22 |
23 |
23 |
24 object JEdit_Resources |
24 object JEdit_Resources |
25 { |
25 { |
26 def apply(options: Options): JEdit_Resources = |
26 def apply(options: Options): JEdit_Resources = |
27 { |
27 new JEdit_Resources(JEdit_Sessions.session_base_info(options)) |
28 val (errs, base) = JEdit_Sessions.session_base(options) |
|
29 new JEdit_Resources(errs, base) |
|
30 } |
|
31 } |
28 } |
32 |
29 |
33 class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base) |
30 class JEdit_Resources private(session_base_info: Sessions.Base_Info) |
34 extends Resources(session_base) |
31 extends Resources(session_base_info.base) |
35 { |
32 { |
|
33 def session_errors: List[String] = session_base_info.errors |
|
34 |
|
35 |
36 /* document node name */ |
36 /* document node name */ |
37 |
37 |
38 def known_file(path: String): Option[Document.Node.Name] = |
38 def known_file(path: String): Option[Document.Node.Name] = |
39 JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true)) |
39 JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true)) |
40 |
40 |