# HG changeset patch
# User wenzelm
# Date 1439335500 -7200
# Node ID 79abcf48c37783bc387c541fc77d65c38ebe3b94
# Parent  d32915a03c63783ac2ab6cea039a165a4e48e0da
clarified init/exit vs. session phase;

diff -r d32915a03c63 -r 79abcf48c377 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 22:17:19 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Wed Aug 12 01:25:00 2015 +0200
@@ -26,7 +26,7 @@
     def set_session(new_session: Session): State =
       copy(session = new_session)
 
-    def is_active: Boolean = active > 0
+    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)
 
@@ -123,12 +123,20 @@
 
   /* protocol commands */
 
-  def set_session(session: Session): Unit =
-    global_state.change(_.set_session(session))
-
   def is_active(): Boolean = global_state.value.is_active
 
-  def inc_active(): Unit =
+  def init_session(session: Session)
+  {
+    global_state.change(state =>
+    {
+      val state1 = state.set_session(session)
+      if (!state.session.is_ready && state1.session.is_ready && state1.is_active)
+        state1.session.protocol_command("Debugger.init")
+      state1
+    })
+  }
+
+  def init(): Unit =
     global_state.change(state =>
     {
       val state1 = state.inc_active
@@ -137,7 +145,7 @@
       state1
     })
 
-  def dec_active(): Unit =
+  def exit(): Unit =
     global_state.change(state =>
     {
       val state1 = state.dec_active
diff -r d32915a03c63 -r 79abcf48c377 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 22:17:19 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 12 01:25:00 2015 +0200
@@ -343,7 +343,6 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        Debugger.set_session(PIDE.session)
         GUI_Thread.later { handle_resize() }
 
       case Debugger.Update =>
@@ -354,8 +353,7 @@
   {
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
-    Debugger.set_session(PIDE.session)
-    Debugger.inc_active()
+    Debugger.init()
     handle_update()
     jEdit.propertiesChanged()
   }
@@ -366,7 +364,7 @@
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
     update_focus(None)
-    Debugger.dec_active()
+    Debugger.exit()
     jEdit.propertiesChanged()
   }
 
diff -r d32915a03c63 -r 79abcf48c377 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 11 22:17:19 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 12 01:25:00 2015 +0200
@@ -262,6 +262,7 @@
         }
 
       case Session.Ready =>
+        Debugger.init_session(PIDE.session)
         PIDE.session.update_options(PIDE.options.value)
         PIDE.init_models()