equal
deleted
inserted
replaced
97 loop { |
97 loop { |
98 react { |
98 react { |
99 case Session.Global_Settings => handle_resize() |
99 case Session.Global_Settings => handle_resize() |
100 case Render(body) => html_panel.render(body) |
100 case Render(body) => html_panel.render(body) |
101 |
101 |
102 case cmd: Command => |
102 case Command_Set(changed) => |
103 Swing_Thread.now { |
103 Swing_Thread.now { |
104 if (follow.selected) Document_Model(view.getBuffer) else None |
104 if (follow.selected) { |
105 } match { |
105 Document_View(view.getTextArea) match { |
106 case None => |
106 case Some(doc_view) => |
107 case Some(model) => |
107 doc_view.selected_command match { |
108 html_panel.render(filtered_results(model.recent_document, cmd)) |
108 case Some(cmd) if changed.contains(cmd) => |
|
109 html_panel.render(filtered_results(doc_view.model.recent_document, cmd)) |
|
110 case _ => |
|
111 } |
|
112 case None => |
|
113 } |
|
114 } |
109 } |
115 } |
110 |
116 |
111 case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
117 case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) |
112 } |
118 } |
113 } |
119 } |
114 } |
120 } |
115 |
121 |
116 override def init() |
122 override def init() |
117 { |
123 { |
118 Isabelle.session.results += main_actor |
124 Isabelle.session.commands_changed += main_actor |
119 Isabelle.session.global_settings += main_actor |
125 Isabelle.session.global_settings += main_actor |
120 } |
126 } |
121 |
127 |
122 override def exit() |
128 override def exit() |
123 { |
129 { |
124 Isabelle.session.results -= main_actor |
130 Isabelle.session.commands_changed -= main_actor |
125 Isabelle.session.global_settings -= main_actor |
131 Isabelle.session.global_settings -= main_actor |
126 } |
132 } |
127 |
133 |
128 |
134 |
129 /* resize */ |
135 /* resize */ |