more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;
--- a/src/Pure/PIDE/session.scala Tue Mar 14 10:49:07 2017 +0100
+++ b/src/Pure/PIDE/session.scala Tue Mar 14 11:16:23 2017 +0100
@@ -443,6 +443,7 @@
case _ if output.is_init =>
phase = Session.Ready
+ debugger.ready()
case Markup.Return_Code(rc) if output.is_exit =>
phase = Session.Terminated(rc)
--- a/src/Pure/Tools/debugger.scala Tue Mar 14 10:49:07 2017 +0100
+++ b/src/Pure/Tools/debugger.scala Tue Mar 14 11:16:23 2017 +0100
@@ -51,7 +51,6 @@
/* debugger state */
sealed case class State(
- session: Session,
active: Int = 0, // active views
break: Boolean = false, // break at next possible breakpoint
active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state
@@ -61,7 +60,7 @@
{
def set_break(b: Boolean): State = copy(break = b)
- def is_active: Boolean = active > 0 && session.is_ready
+ def is_active: Boolean = active > 0
def inc_active: State = copy(active = active + 1)
def dec_active: State = copy(active = active - 1)
@@ -154,7 +153,7 @@
{
/* debugger state */
- private val state = Synchronized(Debugger.State(session))
+ private val state = Synchronized(Debugger.State())
private val delay_update =
Standard_Thread.delay_first(session.output_delay) {
@@ -176,13 +175,19 @@
delay_update.invoke()
}
- def is_active(): Boolean = state.value.is_active
+ def is_active(): Boolean = session.is_ready && state.value.is_active
+
+ def ready()
+ {
+ if (is_active())
+ session.protocol_command("Debugger.init")
+ }
def init(): Unit =
state.change(st =>
{
val st1 = st.inc_active
- if (!st.is_active && st1.is_active)
+ if (session.is_ready && !st.is_active && st1.is_active)
session.protocol_command("Debugger.init")
st1
})
@@ -191,7 +196,7 @@
state.change(st =>
{
val st1 = st.dec_active
- if (st.is_active && !st1.is_active)
+ if (session.is_ready && st.is_active && !st1.is_active)
session.protocol_command("Debugger.exit")
st1
})