--- 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")
}
--- 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()
}