# HG changeset patch
# User wenzelm
# Date 1439653100 -7200
# Node ID 13ee73f57c853f5412a3cda72d6f3a853be46d3f
# Parent  f4bc0400bd1534b0faf7e4b1a462b79dd6f7aee8
allow to break running threads at next possible breakpoint (simplified version of former option, see f3039309702e);

diff -r f4bc0400bd15 -r 13ee73f57c85 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Aug 15 16:47:52 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Sat Aug 15 17:38:20 2015 +0200
@@ -66,6 +66,18 @@
               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 **)
 
@@ -237,7 +249,8 @@
      (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 => ())
@@ -248,6 +261,10 @@
     (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
diff -r f4bc0400bd15 -r 13ee73f57c85 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sat Aug 15 16:47:52 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Sat Aug 15 17:38:20 2015 +0200
@@ -16,9 +16,10 @@
     function: String)
 
   sealed case class State(
-    session: Session = new Session(Resources.empty),
-    active: Int = 0,
-    active_breakpoints: Set[Long] = Set.empty,
+    session: Session = new Session(Resources.empty),  // implicit session
+    active: Int = 0,  // active views
+    break: Boolean = false,  // break at next possible breakpoint
+    active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
     focus: Option[Position.T] = None,  // position of active GUI component
     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
@@ -26,6 +27,8 @@
     def set_session(new_session: Session): State =
       copy(session = new_session)
 
+    def set_break(b: Boolean): State = copy(break = b)
+
     def is_active: Boolean = active > 0 && session.is_ready
     def inc_active: State = copy(active = active + 1)
     def dec_active: State = copy(active = active - 1)
@@ -154,6 +157,17 @@
       state1
     })
 
+  def is_break(): Boolean = global_state.value.break
+  def set_break(b: Boolean)
+  {
+    global_state.change(state => {
+      val state1 = state.set_break(b)
+      state1.session.protocol_command("Debugger.break", b.toString)
+      state1
+    })
+    delay_update.invoke()
+  }
+
   def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   {
     val state = global_state.value
diff -r f4bc0400bd15 -r 13ee73f57c85 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 15 16:47:52 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 15 17:38:20 2015 +0200
@@ -230,6 +230,12 @@
 
   /* controls */
 
+  private val break_button = new CheckBox("Break") {
+    tooltip = "Break running threads at next possible breakpoint"
+    selected = Debugger.is_break()
+    reactions += { case ButtonClicked(_) => Debugger.set_break(selected) }
+  }
+
   private val continue_button = new Button("Continue") {
     tooltip = "Continue program on current thread, until next breakpoint"
     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
@@ -305,7 +311,7 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-      continue_button, step_button, step_over_button, step_out_button,
+      break_button, continue_button, step_button, step_over_button, step_out_button,
       context_label, Component.wrap(context_field),
       expression_label, Component.wrap(expression_field), eval_button, sml_button,
       pretty_text_area.search_label, pretty_text_area.search_field, zoom)
@@ -346,7 +352,10 @@
         GUI_Thread.later { handle_resize() }
 
       case Debugger.Update =>
-        GUI_Thread.later { handle_update() }
+        GUI_Thread.later {
+          break_button.selected = Debugger.is_break()
+          handle_update()
+        }
     }
 
   override def init()