equal
deleted
inserted
replaced
63 class Plugin extends EBPlugin |
63 class Plugin extends EBPlugin |
64 { |
64 { |
65 /* options */ |
65 /* options */ |
66 |
66 |
67 private var _options: JEdit_Options = null |
67 private var _options: JEdit_Options = null |
68 private def init_options(): Unit = _options = new JEdit_Options(Options.init()) |
68 private def init_options(): Unit = |
|
69 _options = new JEdit_Options(Options.init()) |
69 def options: JEdit_Options = _options |
70 def options: JEdit_Options = _options |
70 |
71 |
71 |
72 |
72 /* resources */ |
73 /* resources */ |
73 |
74 |