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