# HG changeset patch
# User wenzelm
# Date 1439293859 -7200
# Node ID 35d85fd89fc1025153261ddef678c08ca55fcced
# Parent  9d8b244234ab2c142f261d3dec2f68618ade86be
eliminated cancel operation: disrupts normal evaluation of thread;

diff -r 9d8b244234ab -r 35d85fd89fc1 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Aug 11 11:55:41 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Aug 11 13:50:59 2015 +0200
@@ -37,40 +37,17 @@
     else error_message (Runtime.exn_message exn);
 
 
-(* thread names and input *)
-
-datatype state =
-  State of {
-    threads: Thread.thread Symtab.table,  (*thread name ~> thread*)
-    input: string list Queue.T Symtab.table  (*thread name ~> input queue*)
-  };
+(* thread input *)
 
-fun make_state (threads, input) = State {threads = threads, input = input};
-val init_state = make_state (Symtab.empty, Symtab.empty);
-fun map_state f (State {threads, input}) = make_state (f (threads, input));
-
-val global_state = Synchronized.var "Debugger.state" init_state;
-
-fun cancel thread_name =
-  Synchronized.change global_state (tap (fn State {threads, ...} =>
-    (case Symtab.lookup threads thread_name of
-      NONE => ()
-    | SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
+val thread_input =
+  Synchronized.var "Debugger.state" (Symtab.empty: string list Queue.T Symtab.table);
 
 fun input thread_name msg =
-  Synchronized.change global_state (map_state (fn (threads, input) =>
-    let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
-    in (threads, input') end));
-
-fun register_thread thread_name =
-  Synchronized.change global_state (map_state (fn (threads, input) =>
-    let
-      val threads' = Symtab.update_new (thread_name, Thread.self ()) threads
-        handle Symtab.DUP _ => threads;
-    in (threads', input) end));
+  Synchronized.change thread_input
+    (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg));
 
 fun get_input thread_name =
-  Synchronized.guarded_access global_state (fn State {threads, input} =>
+  Synchronized.guarded_access thread_input (fn input =>
     (case Symtab.lookup input thread_name of
       NONE => NONE
     | SOME queue =>
@@ -79,7 +56,7 @@
           val input' =
             if Queue.is_empty queue' then Symtab.delete_safe thread_name input
             else Symtab.update (thread_name, queue') input;
-        in SOME (msg, make_state (threads, input')) end));
+        in SOME (msg, input') end));
 
 
 
@@ -226,7 +203,7 @@
         Options.default_bool @{system_option ML_debugger_active}
       then
         (case Simple_Thread.get_name () of
-          SOME thread_name => (register_thread thread_name; debugger_loop thread_name)
+          SOME thread_name => debugger_loop thread_name
         | NONE => ())
       else ()));
 
@@ -267,10 +244,6 @@
       end);
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.cancel"
-    (fn [thread_name] => cancel thread_name);
-
-val _ =
   Isabelle_Process.protocol_command "Debugger.input"
     (fn thread_name :: msg => input thread_name msg);
 
diff -r 9d8b244234ab -r 35d85fd89fc1 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 11:55:41 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 13:50:59 2015 +0200
@@ -168,9 +168,6 @@
   def focus(new_focus: Option[Position.T]): Boolean =
     global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
 
-  def cancel(thread_name: String): Unit =
-    current_state().session.protocol_command("Debugger.cancel", thread_name)
-
   def input(thread_name: String, msg: String*): Unit =
     current_state().session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
 
diff -r 9d8b244234ab -r 35d85fd89fc1 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 11:55:41 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 13:50:59 2015 +0200
@@ -298,11 +298,6 @@
     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
   }
 
-  private val cancel_button = new Button("Cancel") {
-    tooltip = "Interrupt program on current thread"
-    reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.cancel(_)) }
-  }
-
   private val debugger_active =
     new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
 
@@ -310,7 +305,7 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      step_button, step_over_button, step_out_button, continue_button, cancel_button,
+      step_button, step_over_button, step_out_button, continue_button,
       context_label, Component.wrap(context_field),
       expression_label, Component.wrap(expression_field),
       sml_button, eval_button,