# HG changeset patch
# User wenzelm
# Date 1438896015 -7200
# Node ID e78bdf06d33c2a59097fcf6721358b07410e53f2
# Parent  933737bacac71c589ae9e1e3a8458ce1e49a9200
approximate old selection after update;

diff -r 933737bacac7 -r e78bdf06d33c src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 23:08:42 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 23:20:15 2015 +0200
@@ -117,9 +117,10 @@
 
   def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
 
-
   private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
   {
+    val old_thread_selection = thread_selection()
+
     tree.clearSelection
     root.removeAllChildren
 
@@ -134,7 +135,17 @@
     }
 
     tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
+
+    old_thread_selection match {
+      case Some(thread_name) if thread_entries.exists(t => t.thread_name == 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 _ =>
+    }
     for (i <- 0 until tree.getRowCount) tree.expandRow(i)
+
     tree.revalidate()
   }