# HG changeset patch
# User wenzelm
# Date 1438799767 -7200
# Node ID d5d776c8a7e24054c0e4ca427f701e0a19cfc17e
# Parent  6e49311ef842d0be5604e0b12a5ba7a96f63de97
proper dynamic update;

diff -r 6e49311ef842 -r d5d776c8a7e2 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 20:19:51 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 20:36:07 2015 +0200
@@ -12,7 +12,7 @@
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter}
 import javax.swing.{JTree, JScrollPane}
-import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
+import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
 
 import scala.swing.{Button, Label, Component, SplitPane, Orientation}
@@ -80,9 +80,6 @@
     current_snapshot = new_snapshot
     current_threads = new_threads
     current_output = new_output
-
-    revalidate()
-    repaint()
   }
 
 
@@ -97,11 +94,13 @@
   private def update_tree(entries: List[Debugger_Dockable.Tree_Entry])
   {
     tree.clearSelection
+    val tree_model = tree.getModel.asInstanceOf[DefaultTreeModel]
 
     root.removeAllChildren
     val entry_nodes = entries.map(entry => new DefaultMutableTreeNode(entry))
     for (node <- entry_nodes) root.add(node)
 
+    tree_model.reload(root)
     for (i <- 0 until tree.getRowCount) tree.expandRow(i)
 
     for ((entry, node) <- entries zip entry_nodes) {
@@ -110,6 +109,7 @@
         node.add(sub_node)
       }
     }
+    tree_model.reload(root)
 
     tree.revalidate()
   }