--- a/src/Pure/Tools/debugger.scala Thu Nov 07 16:13:58 2024 +0100
+++ b/src/Pure/Tools/debugger.scala Thu Nov 07 20:02:10 2024 +0100
@@ -216,7 +216,7 @@
}
}
- def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = {
+ def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Elem]) = {
val st = state.value
val output =
focus match {
@@ -225,8 +225,8 @@
(for {
(thread_name, results) <- st.output
if thread_name == c.thread_name
- (_, tree) <- results.iterator
- } yield tree).toList
+ (_, msg) <- results.iterator
+ } yield msg).toList
}
(st.threads, output)
}