# HG changeset patch
# User wenzelm
# Date 1670515453 -3600
# Node ID 77805bdabc8eb2a332c0566c4a1a137cf5fbaa82
# Parent  aaedcdfa2154f746bff4edb906d8ee096766ccf4
clarified signature: more robust;

diff -r aaedcdfa2154 -r 77805bdabc8e src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Thu Dec 08 16:10:45 2022 +0100
+++ b/src/Pure/Tools/debugger.scala	Thu Dec 08 17:04:13 2022 +0100
@@ -48,7 +48,7 @@
   /* debugger state */
 
   sealed case class State(
-    active: Int = 0,  // active views
+    active: Set[AnyRef] = Set.empty,  // active views
     break: Boolean = false,  // break at next possible breakpoint
     active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
     threads: Threads = SortedMap.empty,  // thread name ~> stack of debug states
@@ -57,9 +57,9 @@
   ) {
     def set_break(b: Boolean): State = copy(break = b)
 
-    def is_active: Boolean = active > 0
-    def inc_active: State = copy(active = active + 1)
-    def dec_active: State = copy(active = active - 1)
+    def is_active: Boolean = active.nonEmpty
+    def register_active(id: AnyRef): State = copy(active = active + id)
+    def unregister_active(id: AnyRef): State = copy(active = active - id)
 
     def toggle_breakpoint(breakpoint: Long): (Boolean, State) = {
       val active_breakpoints1 =
@@ -167,18 +167,18 @@
   def ready(): Unit =
     if (is_active()) session.protocol_command("Debugger.init")
 
-  def init(): Unit =
+  def init(id: AnyRef): Unit =
     state.change { st =>
-      val st1 = st.inc_active
+      val st1 = st.register_active(id)
       if (session.is_ready && !st.is_active && st1.is_active) {
         session.protocol_command("Debugger.init")
       }
       st1
     }
 
-  def exit(): Unit =
+  def exit(id: AnyRef): Unit =
     state.change { st =>
-      val st1 = st.dec_active
+      val st1 = st.unregister_active(id)
       if (session.is_ready && st.is_active && !st1.is_active) {
         session.protocol_command("Debugger.exit")
       }
diff -r aaedcdfa2154 -r 77805bdabc8e src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Dec 08 16:10:45 2022 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Dec 08 17:04:13 2022 +0100
@@ -53,6 +53,8 @@
 }
 
 class Debugger_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
   private val debugger = PIDE.session.debugger
@@ -320,7 +322,7 @@
   override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
-    debugger.init()
+    debugger.init(dockable)
     handle_update()
     jEdit.propertiesChanged()
   }
@@ -329,7 +331,7 @@
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
-    debugger.exit()
+    debugger.exit(dockable)
     jEdit.propertiesChanged()
   }