# HG changeset patch
# User wenzelm
# Date 1489486583 -3600
# Node ID 844c067bc3d4e8a784192bbde1607f80a9f9c9fe
# Parent  fb82535644834e1da0dbc63f87e872cb054777c5
more robust startup, despite remaining race condition of debugger.is_active vs. session.is_ready;

diff -r fb8253564483 -r 844c067bc3d4 src/Pure/PIDE/session.scala
--- 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)
diff -r fb8253564483 -r 844c067bc3d4 src/Pure/Tools/debugger.scala
--- 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
     })