# HG changeset patch # User wenzelm # Date 1489524886 -3600 # Node ID 63d91d5de121fa6e95d2a0ac5f620d9d1c67814c # Parent 848965b5befc7057879d83aa70da89469c59dbbd tuned signature; diff -r 848965b5befc -r 63d91d5de121 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Mar 14 21:43:54 2017 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Mar 14 21:54:46 2017 +0100 @@ -47,7 +47,7 @@ /* context menu */ def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = - if (PIDE.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) { + if (PIDE.session.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) { val context = jEdit.getActionContext() val name = "isabelle.toggle-breakpoint" List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context)) @@ -59,6 +59,8 @@ { GUI_Thread.require {} + private val debugger = PIDE.session.debugger + /* component state -- owned by GUI thread */ @@ -86,7 +88,7 @@ GUI_Thread.require {} val new_snapshot = JEdit_Editor.current_node_snapshot(view).getOrElse(current_snapshot) - val (new_threads, new_output) = PIDE.debugger.status(tree_selection()) + val (new_threads, new_output) = debugger.status(tree_selection()) if (new_threads != current_threads) update_tree(new_threads) @@ -165,9 +167,9 @@ { tree_selection() match { case Some(c) if c.stack_state.isDefined => - PIDE.debugger.print_vals(c, sml_button.selected, context_field.getText) + debugger.print_vals(c, sml_button.selected, context_field.getText) case Some(c) => - PIDE.debugger.clear_output(c.thread_name) + debugger.clear_output(c.thread_name) case None => } } @@ -199,28 +201,28 @@ private val break_button = new CheckBox("Break") { tooltip = "Break running threads at next possible breakpoint" - selected = PIDE.debugger.is_break() - reactions += { case ButtonClicked(_) => PIDE.debugger.set_break(selected) } + selected = debugger.is_break() + reactions += { case ButtonClicked(_) => debugger.set_break(selected) } } private val continue_button = new Button("Continue") { tooltip = "Continue program on current thread, until next breakpoint" - reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.continue(_)) } + reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue(_)) } } private val step_button = new Button("Step") { tooltip = "Single-step in depth-first order" - reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step(_)) } + reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step(_)) } } private val step_over_button = new Button("Step over") { tooltip = "Single-step within this function" - reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_over(_)) } + reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over(_)) } } private val step_out_button = new Button("Step out") { tooltip = "Single-step outside this function" - reactions += { case ButtonClicked(_) => thread_selection().map(PIDE.debugger.step_out(_)) } + reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out(_)) } } private val context_label = new Label("Context:") { @@ -269,7 +271,7 @@ expression_field.addCurrentToHistory() tree_selection() match { case Some(c) if c.debug_index.isDefined => - PIDE.debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) + debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) case _ => } } @@ -301,7 +303,7 @@ private def update_focus() { for (c <- tree_selection()) { - PIDE.debugger.set_focus(c) + debugger.set_focus(c) for { pos <- c.debug_position link <- JEdit_Editor.hyperlink_position(false, current_snapshot, pos) @@ -330,7 +332,7 @@ case Debugger.Update => GUI_Thread.later { - break_button.selected = PIDE.debugger.is_break() + break_button.selected = debugger.is_break() handle_update() } } @@ -339,7 +341,7 @@ { PIDE.session.global_options += main PIDE.session.debugger_updates += main - PIDE.debugger.init() + debugger.init() handle_update() jEdit.propertiesChanged() } @@ -349,7 +351,7 @@ PIDE.session.global_options -= main PIDE.session.debugger_updates -= main delay_resize.revoke() - PIDE.debugger.exit() + debugger.exit() jEdit.propertiesChanged() } diff -r 848965b5befc -r 63d91d5de121 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Mar 14 21:43:54 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Mar 14 21:54:46 2017 +0100 @@ -442,10 +442,10 @@ { GUI_Thread.require {} - if (PIDE.debugger.is_active()) { + if (PIDE.session.debugger.is_active()) { Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition) match { case Some((command, breakpoint)) => - PIDE.debugger.toggle_breakpoint(command, breakpoint) + PIDE.session.debugger.toggle_breakpoint(command, breakpoint) jEdit.propertiesChanged() case None => } diff -r 848965b5befc -r 63d91d5de121 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 14 21:43:54 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 14 21:54:46 2017 +0100 @@ -456,7 +456,7 @@ snapshot.select(range, JEdit_Rendering.bullet_elements, _ => { case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => - PIDE.debugger.active_breakpoint_state(breakpoint).map(b => + PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b => if (b) breakpoint_enabled_color else breakpoint_disabled_color) case _ => Some(bullet_color) }) diff -r 848965b5befc -r 63d91d5de121 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:43:54 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:54:46 2017 +0100 @@ -41,8 +41,6 @@ def resources(): JEdit_Resources = session.resources.asInstanceOf[JEdit_Resources] - def debugger: Debugger = session.debugger - /* current document content */ diff -r 848965b5befc -r 63d91d5de121 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Tue Mar 14 21:43:54 2017 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Mar 14 21:54:46 2017 +0100 @@ -371,7 +371,7 @@ else { val debug_positions = (for { - c <- PIDE.debugger.focus().iterator + c <- PIDE.session.debugger.focus().iterator pos <- c.debug_position.iterator } yield pos).toList if (debug_positions.exists(JEdit_Editor.is_hyperlink_position(rendering.snapshot, offset, _)))