# HG changeset patch
# User wenzelm
# Date 1438864139 -7200
# Node ID 8f45dd297357be8bb1ed4ca8c9aa1d5959202c6f
# Parent  b0627cb2e08d10d4a54a4d45f7d7574c8414147f
more controls;

diff -r b0627cb2e08d -r 8f45dd297357 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Thu Aug 06 14:23:59 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Thu Aug 06 14:28:59 2015 +0200
@@ -119,9 +119,11 @@
     current_state().session.protocol_command("Debugger.init")
   }
 
-  def cancel(name: String): Unit =
-    current_state().session.protocol_command("Debugger.cancel", name)
+  def cancel(thread_name: String): Unit =
+    current_state().session.protocol_command("Debugger.cancel", thread_name)
 
-  def input(name: String, msg: String*): Unit =
-    current_state().session.protocol_command("Debugger.input", (name :: msg.toList):_*)
+  def input(thread_name: String, msg: String*): Unit =
+    current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
+
+  def continue(thread_name: String): Unit = input(thread_name, "continue")
 }
diff -r b0627cb2e08d -r 8f45dd297357 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 14:23:59 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 14:28:59 2015 +0200
@@ -70,7 +70,7 @@
     val new_threads = new_state.threads
     val new_output =
     {
-      val thread_selection = tree_selection().map(_._1)
+      val thread_selection = tree_selection().map(sel => sel._1.thread_name)
       (for {
         (thread_name, results) <- new_state.output
         if thread_selection.isEmpty || thread_selection.get == thread_name
@@ -102,15 +102,15 @@
   tree.setRowHeight(0)
   tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
 
-  def tree_selection(): Option[(String, Option[Int])] =
+  def tree_selection(): Option[(Debugger_Dockable.Thread_Entry, Option[Int])] =
     tree.getSelectionPath match {
       case null => None
       case path =>
         path.getPath.toList.map(n => n.asInstanceOf[DefaultMutableTreeNode].getUserObject) match {
           case List(_, t: Debugger_Dockable.Thread_Entry) =>
-            Some((t.thread_name, None))
+            Some((t, None))
           case List(_, t: Debugger_Dockable.Thread_Entry, s: Debugger_Dockable.Stack_Entry) =>
-            Some((t.thread_name, Some(s.index)))
+            Some((t, Some(s.index)))
           case _ => None
         }
     }
@@ -201,6 +201,28 @@
       quote(expression_field.getText))
   }
 
+  private val continue_button = new Button("Continue") {
+      tooltip = "Continue program on current thread, until next breakpoint"
+      reactions += {
+        case ButtonClicked(_) =>
+          tree_selection() match {
+            case Some((t, _)) => Debugger.continue(t.thread_name)
+            case _ =>
+          }
+      }
+    }
+
+  private val cancel_button = new Button("Cancel") {
+      tooltip = "Interrupt program on current thread"
+      reactions += {
+        case ButtonClicked(_) =>
+          tree_selection() match {
+            case Some((t, _)) => Debugger.cancel(t.thread_name)
+            case _ =>
+          }
+      }
+    }
+
   private val debugger_active =
     new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
 
@@ -213,6 +235,7 @@
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       context_label, Component.wrap(context_field),
       expression_label, Component.wrap(expression_field), eval_button,
+      continue_button, cancel_button,
       pretty_text_area.search_label, pretty_text_area.search_field,
       debugger_stepping, debugger_active, zoom)
   add(controls.peer, BorderLayout.NORTH)