# HG changeset patch
# User wenzelm
# Date 1439323585 -7200
# Node ID 6032429da70d1c2280991f64f2b9ed25d7c6c933
# Parent  eba3acb72b5550e982b446ccc67531f5db17f49d
clarified thread re-selection;

diff -r eba3acb72b55 -r 6032429da70d src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 22:01:11 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 22:06:25 2015 +0200
@@ -166,8 +166,12 @@
 
   private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
   {
-    val old_thread_selection: Option[String] =
-      thread_selection() orElse thread_entries.headOption.map(_.thread_name)
+    val new_thread_selection =
+      thread_selection() match {
+        case Some(thread_name) if thread_entries.exists(t => t.thread_name == thread_name) =>
+          Some(thread_name)
+        case _ => thread_entries.headOption.map(_.thread_name)
+      }
 
     tree.clearSelection
     root.removeAllChildren
@@ -187,13 +191,13 @@
     tree.expandRow(0)
     for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i)
 
-    old_thread_selection match {
-      case Some(thread_name) if thread_entries.exists(t => t.thread_name == thread_name) =>
+    new_thread_selection match {
+      case Some(thread_name) =>
         val i =
           (for (t <- thread_entries.iterator.takeWhile(t => t.thread_name != thread_name))
             yield 1 + t.debug_states.length).sum
         tree.addSelectionRow(i + 1)
-      case _ =>
+      case None =>
     }
 
     tree.revalidate()