equal
deleted
inserted
replaced
35 if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin") |
35 if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin") |
36 else _plugin |
36 else _plugin |
37 def options: JEdit_Options = plugin.options |
37 def options: JEdit_Options = plugin.options |
38 |
38 |
39 @volatile var session: Session = new Session(JEdit_Resources.empty) |
39 @volatile var session: Session = new Session(JEdit_Resources.empty) |
40 |
|
41 def options_changed() { if (plugin != null) plugin.options_changed() } |
|
42 def deps_changed() { if (plugin != null) plugin.deps_changed() } |
|
43 |
40 |
44 def resources(): JEdit_Resources = |
41 def resources(): JEdit_Resources = |
45 session.resources.asInstanceOf[JEdit_Resources] |
42 session.resources.asInstanceOf[JEdit_Resources] |
46 |
43 |
47 def debugger: Debugger = session.debugger |
44 def debugger: Debugger = session.debugger |