--- 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