--- 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()
}
--- 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 =>
}
--- 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)
})
--- 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 */
--- 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, _)))