approximate old selection after update;
authorwenzelm
Thu, 06 Aug 2015 23:20:15 +0200
changeset 60860 e78bdf06d33c
parent 60859 933737bacac7
child 60861 fa77faa87d5f
approximate old selection after update;
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()
   }