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