equal
deleted
inserted
replaced
34 |
34 |
35 @volatile var startup_failure: Option[Throwable] = None |
35 @volatile var startup_failure: Option[Throwable] = None |
36 @volatile var startup_notified = false |
36 @volatile var startup_notified = false |
37 |
37 |
38 @volatile var plugin: Plugin = null |
38 @volatile var plugin: Plugin = null |
39 @volatile var session: Session = |
39 @volatile var session: Session = new Session(JEdit_Resources.empty) |
40 new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty)) |
|
41 |
40 |
42 def options_changed() { plugin.options_changed() } |
41 def options_changed() { plugin.options_changed() } |
43 def deps_changed() { plugin.deps_changed() } |
42 def deps_changed() { plugin.deps_changed() } |
44 |
43 |
45 def resources(): JEdit_Resources = |
44 def resources(): JEdit_Resources = |