src/Pure/Tools/debugger.scala
changeset 61018 32cc7d219c38
parent 61016 7c5a877b0f8e
child 61019 7ce030f14aa9
--- a/src/Pure/Tools/debugger.scala	Mon Aug 24 20:08:00 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 24 20:32:32 2015 +0200
@@ -227,7 +227,21 @@
     })
   }
 
-  def threads(): Threads = global_state.value.threads
+  def status(focus: Option[Context]): (Threads, List[XML.Tree]) =
+  {
+    val state = global_state.value
+    val output =
+      focus match {
+        case None => Nil
+        case Some(c) =>
+          (for {
+            (thread_name, results) <- state.output
+            if thread_name == c.thread_name
+            (_, tree) <- results.iterator
+          } yield tree).toList
+      }
+    (state.threads, output)
+  }
 
   def focus(): List[Context] = global_state.value.focus.toList.map(_._2)
   def set_focus(c: Context)
@@ -236,8 +250,6 @@
     delay_update.invoke()
   }
 
-  def output(): Map[String, Command.Results] = global_state.value.output
-
   def input(thread_name: String, msg: String*): Unit =
     global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)