# HG changeset patch
# User wenzelm
# Date 1731006130 -3600
# Node ID 4ee8da9e48ea85d25c6dbc73fca8e7db1107ab5a
# Parent  92aa6f7b470cfc808407d0b5b1c8412ae46cd957
clarified signature;

diff -r 92aa6f7b470c -r 4ee8da9e48ea src/Pure/Tools/debugger.scala
--- 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)
   }