32 |
32 |
33 def toggle_breakpoint(command: Command, breakpoint: Long) |
33 def toggle_breakpoint(command: Command, breakpoint: Long) |
34 { |
34 { |
35 GUI_Thread.require {} |
35 GUI_Thread.require {} |
36 |
36 |
37 Debugger.toggle_breakpoint(command, breakpoint) |
37 PIDE.debugger.toggle_breakpoint(command, breakpoint) |
38 jEdit.propertiesChanged() |
38 jEdit.propertiesChanged() |
39 } |
39 } |
40 |
40 |
41 def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] = |
41 def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] = |
42 { |
42 { |
53 |
53 |
54 |
54 |
55 /* context menu */ |
55 /* context menu */ |
56 |
56 |
57 def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
57 def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
58 if (Debugger.is_active() && get_breakpoint(text_area, offset).isDefined) { |
58 if (PIDE.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) { |
59 val context = jEdit.getActionContext() |
59 val context = jEdit.getActionContext() |
60 val name = "isabelle.toggle-breakpoint" |
60 val name = "isabelle.toggle-breakpoint" |
61 List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context)) |
61 List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context)) |
62 } |
62 } |
63 else Nil |
63 else Nil |
92 private def handle_update() |
92 private def handle_update() |
93 { |
93 { |
94 GUI_Thread.require {} |
94 GUI_Thread.require {} |
95 |
95 |
96 val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) |
96 val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) |
97 val (new_threads, new_output) = Debugger.status(tree_selection()) |
97 val (new_threads, new_output) = PIDE.debugger.status(tree_selection()) |
98 |
98 |
99 if (new_threads != current_threads) |
99 if (new_threads != current_threads) |
100 update_tree(new_threads) |
100 update_tree(new_threads) |
101 |
101 |
102 if (new_output != current_output) |
102 if (new_output != current_output) |
171 |
171 |
172 def update_vals() |
172 def update_vals() |
173 { |
173 { |
174 tree_selection() match { |
174 tree_selection() match { |
175 case Some(c) if c.stack_state.isDefined => |
175 case Some(c) if c.stack_state.isDefined => |
176 Debugger.print_vals(c, sml_button.selected, context_field.getText) |
176 PIDE.debugger.print_vals(c, sml_button.selected, context_field.getText) |
177 case Some(c) => |
177 case Some(c) => |
178 Debugger.clear_output(c.thread_name) |
178 PIDE.debugger.clear_output(c.thread_name) |
179 case None => |
179 case None => |
180 } |
180 } |
181 } |
181 } |
182 |
182 |
183 tree.addTreeSelectionListener( |
183 tree.addTreeSelectionListener( |
205 |
205 |
206 /* controls */ |
206 /* controls */ |
207 |
207 |
208 private val break_button = new CheckBox("Break") { |
208 private val break_button = new CheckBox("Break") { |
209 tooltip = "Break running threads at next possible breakpoint" |
209 tooltip = "Break running threads at next possible breakpoint" |
210 selected = Debugger.is_break() |
210 selected = PIDE.debugger.is_break() |
211 reactions += { case ButtonClicked(_) => Debugger.set_break(selected) } |
211 reactions += { case ButtonClicked(_) => PIDE.debugger.set_break(selected) } |
212 } |
212 } |
213 |
213 |
214 private val continue_button = new Button("Continue") { |
214 private val continue_button = new Button("Continue") { |
215 tooltip = "Continue program on current thread, until next breakpoint" |
215 tooltip = "Continue program on current thread, until next breakpoint" |
216 reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) } |
216 reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.continue(_)) } |
217 } |
217 } |
218 |
218 |
219 private val step_button = new Button("Step") { |
219 private val step_button = new Button("Step") { |
220 tooltip = "Single-step in depth-first order" |
220 tooltip = "Single-step in depth-first order" |
221 reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step(_)) } |
221 reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step(_)) } |
222 } |
222 } |
223 |
223 |
224 private val step_over_button = new Button("Step over") { |
224 private val step_over_button = new Button("Step over") { |
225 tooltip = "Single-step within this function" |
225 tooltip = "Single-step within this function" |
226 reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_over(_)) } |
226 reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_over(_)) } |
227 } |
227 } |
228 |
228 |
229 private val step_out_button = new Button("Step out") { |
229 private val step_out_button = new Button("Step out") { |
230 tooltip = "Single-step outside this function" |
230 tooltip = "Single-step outside this function" |
231 reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) } |
231 reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_out(_)) } |
232 } |
232 } |
233 |
233 |
234 private val context_label = new Label("Context:") { |
234 private val context_label = new Label("Context:") { |
235 tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic" |
235 tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic" |
236 } |
236 } |
275 { |
275 { |
276 context_field.addCurrentToHistory() |
276 context_field.addCurrentToHistory() |
277 expression_field.addCurrentToHistory() |
277 expression_field.addCurrentToHistory() |
278 tree_selection() match { |
278 tree_selection() match { |
279 case Some(c) if c.debug_index.isDefined => |
279 case Some(c) if c.debug_index.isDefined => |
280 Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) |
280 PIDE.debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) |
281 case _ => |
281 case _ => |
282 } |
282 } |
283 } |
283 } |
284 |
284 |
285 private val sml_button = new CheckBox("SML") { |
285 private val sml_button = new CheckBox("SML") { |
307 }) |
307 }) |
308 |
308 |
309 private def update_focus() |
309 private def update_focus() |
310 { |
310 { |
311 for (c <- tree_selection()) { |
311 for (c <- tree_selection()) { |
312 Debugger.set_focus(c) |
312 PIDE.debugger.set_focus(c) |
313 for { |
313 for { |
314 pos <- c.debug_position |
314 pos <- c.debug_position |
315 link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos) |
315 link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos) |
316 } link.follow(view) |
316 } link.follow(view) |
317 } |
317 } |
336 case _: Session.Global_Options => |
336 case _: Session.Global_Options => |
337 GUI_Thread.later { handle_resize() } |
337 GUI_Thread.later { handle_resize() } |
338 |
338 |
339 case Debugger.Update => |
339 case Debugger.Update => |
340 GUI_Thread.later { |
340 GUI_Thread.later { |
341 break_button.selected = Debugger.is_break() |
341 break_button.selected = PIDE.debugger.is_break() |
342 handle_update() |
342 handle_update() |
343 } |
343 } |
344 } |
344 } |
345 |
345 |
346 override def init() |
346 override def init() |
347 { |
347 { |
348 PIDE.session.global_options += main |
348 PIDE.session.global_options += main |
349 PIDE.session.debugger_updates += main |
349 PIDE.session.debugger_updates += main |
350 Debugger.init() |
350 PIDE.debugger.init() |
351 handle_update() |
351 handle_update() |
352 jEdit.propertiesChanged() |
352 jEdit.propertiesChanged() |
353 } |
353 } |
354 |
354 |
355 override def exit() |
355 override def exit() |
356 { |
356 { |
357 PIDE.session.global_options -= main |
357 PIDE.session.global_options -= main |
358 PIDE.session.debugger_updates -= main |
358 PIDE.session.debugger_updates -= main |
359 delay_resize.revoke() |
359 delay_resize.revoke() |
360 Debugger.exit() |
360 PIDE.debugger.exit() |
361 jEdit.propertiesChanged() |
361 jEdit.propertiesChanged() |
362 } |
362 } |
363 |
363 |
364 |
364 |
365 /* resize */ |
365 /* resize */ |