109 private val main = |
109 private val main = |
110 Session.Consumer[Any](getClass.getName) { |
110 Session.Consumer[Any](getClass.getName) { |
111 case _: Session.Global_Options => |
111 case _: Session.Global_Options => |
112 GUI_Thread.later { handle_resize() } |
112 GUI_Thread.later { handle_resize() } |
113 |
113 |
|
114 case changed: Session.Commands_Changed => |
|
115 if (changed.assignment) GUI_Thread.later { maybe_update() } |
|
116 |
114 case Session.Caret_Focus => |
117 case Session.Caret_Focus => |
115 GUI_Thread.later { maybe_update() } |
118 GUI_Thread.later { maybe_update() } |
116 } |
119 } |
117 |
120 |
118 override def init() |
121 override def init() |
119 { |
122 { |
120 PIDE.session.global_options += main |
123 PIDE.session.global_options += main |
|
124 PIDE.session.commands_changed += main |
121 PIDE.session.caret_focus += main |
125 PIDE.session.caret_focus += main |
122 handle_resize() |
126 handle_resize() |
123 print_state.activate() |
127 print_state.activate() |
|
128 maybe_update() |
124 } |
129 } |
125 |
130 |
126 override def exit() |
131 override def exit() |
127 { |
132 { |
128 print_state.deactivate() |
133 print_state.deactivate() |
129 PIDE.session.caret_focus -= main |
134 PIDE.session.caret_focus -= main |
130 PIDE.session.global_options -= main |
135 PIDE.session.global_options -= main |
|
136 PIDE.session.commands_changed -= main |
131 delay_resize.revoke() |
137 delay_resize.revoke() |
132 } |
138 } |
133 } |
139 } |