# HG changeset patch
# User wenzelm
# Date 1439286941 -7200
# Node ID 9d8b244234ab2c142f261d3dec2f68618ade86be
# Parent  0165aac83cdbfcf6b6d6a10199af2ff94c744f87
register thread such that cancel works;

diff -r 0165aac83cdb -r 9d8b244234ab src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Aug 10 22:34:00 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Aug 11 11:55:41 2015 +0200
@@ -62,6 +62,13 @@
     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));
+
 fun get_input thread_name =
   Synchronized.guarded_access global_state (fn State {threads, input} =>
     (case Symtab.lookup input thread_name of
@@ -215,12 +222,11 @@
 fun init () =
   ML_Debugger.on_breakpoint
     (SOME (fn (_, break) =>
-      if not (is_debugging ()) andalso
-        (! break orelse is_stepping ()) andalso
+      if not (is_debugging ()) andalso (! break orelse is_stepping ()) andalso
         Options.default_bool @{system_option ML_debugger_active}
       then
         (case Simple_Thread.get_name () of
-          SOME thread_name => debugger_loop thread_name
+          SOME thread_name => (register_thread thread_name; debugger_loop thread_name)
         | NONE => ())
       else ()));