equal
deleted
inserted
replaced
127 |
127 |
128 private val main = |
128 private val main = |
129 Session.Consumer[Any](getClass.getName) { |
129 Session.Consumer[Any](getClass.getName) { |
130 case _: Session.Global_Options => |
130 case _: Session.Global_Options => |
131 GUI_Thread.later { |
131 GUI_Thread.later { |
|
132 handle_resize() |
132 output_state_button.selected = output_state |
133 output_state_button.selected = output_state |
133 handle_update(do_update, None) |
134 handle_update(do_update, None) |
134 } |
135 } |
135 |
136 |
136 case changed: Session.Commands_Changed => |
137 case changed: Session.Commands_Changed => |