clarified signature;
authorwenzelm
Thu, 07 Nov 2024 20:02:10 +0100
changeset 81393 4ee8da9e48ea
parent 81392 92aa6f7b470c
child 81394 95b53559af80
clarified signature;
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)
   }