src/Pure/Tools/debugger.ML

                 val (msg, queue') = Queue.dequeue queue;
                 val input' =
                   if Queue.is_empty queue' then Symtab.delete_safe thread_name input
                   else Symtab.update (thread_name, queue') input;
               in SOME (msg, SOME input') end));
+
+
+(* global break *)
+
+local
+  val break = Synchronized.var "Debugger.break" false;
+in
+
+fun is_break () = Synchronized.value break;
+fun set_break b = Synchronized.change break (K b);
+
+end;
 
 
 
 (** thread state **)
 

   Isabelle_Process.protocol_command "Debugger.init"
     (fn [] =>
      (init_input ();
       ML_Debugger.on_breakpoint
         (SOME (fn (_, break) =>
-          if not (is_debugging ()) andalso (! break orelse is_stepping ()) then
+          if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
+          then
             (case Simple_Thread.get_name () of
               SOME thread_name => debugger_loop thread_name
             | NONE => ())
           else ()))));
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.exit"
     (fn [] => (ML_Debugger.on_breakpoint NONE; exit_input ()));
+
+val _ =
+  Isabelle_Process.protocol_command "Debugger.break"
+    (fn [b] => set_break (Markup.parse_bool b));
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.breakpoint"
     (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
       let