# HG changeset patch
# User wenzelm
# Date 1439317691 -7200
# Node ID 84569dbe1e308db4ca7b7f26c7b996b7e0b4a2d5
# Parent  a3fcde62df107773337c7c1a3eb23ca220d2245b
tuned;

diff -r a3fcde62df10 -r 84569dbe1e30 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 20:21:13 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 20:28:11 2015 +0200
@@ -188,10 +188,10 @@
   def input(thread_name: String, msg: String*): Unit =
     global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
 
+  def continue(thread_name: String): Unit = input(thread_name, "continue")
   def step(thread_name: String): Unit = input(thread_name, "step")
   def step_over(thread_name: String): Unit = input(thread_name, "step_over")
   def step_out(thread_name: String): Unit = input(thread_name, "step_out")
-  def continue(thread_name: String): Unit = input(thread_name, "continue")
 
   def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String)
   {
diff -r a3fcde62df10 -r 84569dbe1e30 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 20:21:13 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 20:28:11 2015 +0200
@@ -287,6 +287,11 @@
     }
   }
 
+  private val continue_button = new Button("Continue") {
+    tooltip = "Continue program on current thread, until next breakpoint"
+    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(Debugger.step(_)) }
@@ -302,16 +307,11 @@
     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.step_out(_)) }
   }
 
-  private val continue_button = new Button("Continue") {
-    tooltip = "Continue program on current thread, until next breakpoint"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
-  }
-
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      step_button, step_over_button, step_out_button, continue_button,
+      continue_button, step_button, step_over_button, step_out_button,
       context_label, Component.wrap(context_field),
       expression_label, Component.wrap(expression_field), sml_button, eval_button,
       pretty_text_area.search_label, pretty_text_area.search_field, zoom)