80 current_results = new_results |
78 current_results = new_results |
81 current_output = new_output |
79 current_output = new_output |
82 } |
80 } |
83 |
81 |
84 |
82 |
85 /* main actor */ |
83 /* main */ |
86 |
84 |
87 private val main_actor = actor { |
85 private val main = |
88 loop { |
86 Session.Consumer[Any](getClass.getName) { |
89 react { |
87 case _: Session.Global_Options => |
90 case _: Session.Global_Options => |
88 Swing_Thread.later { handle_resize() } |
91 Swing_Thread.later { handle_resize() } |
|
92 |
89 |
93 case changed: Session.Commands_Changed => |
90 case changed: Session.Commands_Changed => |
94 val restriction = if (changed.assignment) None else Some(changed.commands) |
91 val restriction = if (changed.assignment) None else Some(changed.commands) |
95 Swing_Thread.later { handle_update(do_update, restriction) } |
92 Swing_Thread.later { handle_update(do_update, restriction) } |
96 |
93 |
97 case Session.Caret_Focus => |
94 case Session.Caret_Focus => |
98 Swing_Thread.later { handle_update(do_update, None) } |
95 Swing_Thread.later { handle_update(do_update, None) } |
99 |
|
100 case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
|
101 } |
|
102 } |
96 } |
103 } |
|
104 |
97 |
105 override def init() |
98 override def init() |
106 { |
99 { |
107 PIDE.session.global_options += main_actor |
100 PIDE.session.global_options += main |
108 PIDE.session.commands_changed += main_actor |
101 PIDE.session.commands_changed += main |
109 PIDE.session.caret_focus += main_actor |
102 PIDE.session.caret_focus += main |
110 handle_update(true, None) |
103 handle_update(true, None) |
111 } |
104 } |
112 |
105 |
113 override def exit() |
106 override def exit() |
114 { |
107 { |
115 PIDE.session.global_options -= main_actor |
108 PIDE.session.global_options -= main |
116 PIDE.session.commands_changed -= main_actor |
109 PIDE.session.commands_changed -= main |
117 PIDE.session.caret_focus -= main_actor |
110 PIDE.session.caret_focus -= main |
118 delay_resize.revoke() |
111 delay_resize.revoke() |
119 } |
112 } |
120 |
113 |
121 |
114 |
122 /* resize */ |
115 /* resize */ |