# HG changeset patch
# User wenzelm
# Date 1440441152 -7200
# Node ID 32cc7d219c38f48154a21cf444e2562ae43889ed
# Parent  a538a03972d21fec384823b57cf8a5dbe2494dd6
atomic Debugger.status;
output without thread context is empty;
tuned;

diff -r a538a03972d2 -r 32cc7d219c38 src/Pure/Tools/debugger.scala
--- 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):_*)
 
diff -r a538a03972d2 -r 32cc7d219c38 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 20:08:00 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 20:32:32 2015 +0200
@@ -94,24 +94,10 @@
     GUI_Thread.require {}
 
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
-    val new_threads = Debugger.threads()
-    val new_output =
-    {
-      val output = Debugger.output()
-      val current_thread_selection = thread_selection()
-      (for {
-        (thread_name, results) <- output
-        if current_thread_selection.isEmpty || current_thread_selection.get == thread_name
-        (_, tree) <- results.iterator
-      } yield tree).toList
-    }
+    val (new_threads, new_output) = Debugger.status(tree_selection())
 
-    if (new_threads != current_threads) {
-      val threads =
-        (for ((a, b) <- new_threads.iterator)
-          yield Debugger.Context(a, b)).toList
-      update_tree(threads)
-    }
+    if (new_threads != current_threads)
+      update_tree(new_threads)
 
     if (new_output != current_output)
       pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
@@ -142,21 +128,24 @@
 
   def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
-  private def update_tree(threads: List[Debugger.Context])
+  private def update_tree(threads: Debugger.Threads)
   {
-    require(threads.forall(_.index == 0))
+    val thread_contexts =
+      (for ((a, b) <- threads.iterator)
+        yield Debugger.Context(a, b)).toList
 
     val new_tree_selection =
       tree_selection() match {
-        case Some(c) if threads.contains(c) => Some(c)
-        case Some(c) if threads.exists(t => c.thread_name == t.thread_name) => Some(c.reset)
-        case _ => threads.headOption
+        case Some(c) if thread_contexts.contains(c) => Some(c)
+        case Some(c) if thread_contexts.exists(t => c.thread_name == t.thread_name) =>
+          Some(c.reset)
+        case _ => thread_contexts.headOption
       }
 
     tree.clearSelection
     root.removeAllChildren
 
-    for (thread <- threads) {
+    for (thread <- thread_contexts) {
       val thread_node = new DefaultMutableTreeNode(thread)
       for ((debug_state, i) <- thread.debug_states.zipWithIndex)
         thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
@@ -171,7 +160,7 @@
     new_tree_selection match {
       case Some(c) =>
         val i =
-          (for (t <- threads.iterator.takeWhile(t => c.thread_name != t.thread_name))
+          (for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name))
             yield t.size).sum
         tree.addSelectionRow(i + c.index + 1)
       case None =>