Fix various UI bugs

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java

@@ -38,6 +38,7 @@
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.java.SwingUtil;
 
 import bibliothek.gui.dock.common.action.CAction;
 import org.slf4j.Logger;
@@ -678,6 +679,10 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) {
             return false;
         }
 
+        // Save expansion state to restore.
+        List<TreePath> rowsToExpand = new ArrayList<>(expansionState);
+
+
         final TreePath branch;
         final Node invokedNode;
         if (selectedPath.getLastPathComponent() instanceof GUIProofTreeNode) {
@@ -741,6 +746,12 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) {
                 delegateView.setSelectionPath(tp);
             }
         }
+
+        // Expand previously visible rows.
+        for (TreePath tp : rowsToExpand) {
+            TreePath newTp = SwingUtil.findPathInNewTree(delegateView, tp);
+            delegateView.expandPath(newTp);
+        }
         return true;
     }
 

key.ui/src/main/java/org/key_project/util/java/SwingUtil.java

@@ -9,6 +9,7 @@
 import java.util.List;
 import java.util.Set;
 import javax.swing.*;
+import javax.swing.tree.TreePath;
 
 import bibliothek.gui.dock.themes.basic.BasicDockableDisplayer;
 
@@ -149,4 +150,46 @@ public static JScrollPane createScrollPane(JTable table) {
 
         return scrollPane;
     }
+
+    /**
+     * Try to find a tree path after updating the nodes of a {@link JTree}.
+     * This will compare nodes by their string representation.
+     *
+     * @param tree the tree to search
+     * @param tp the tree path
+     * @return a tree path or null
+     */
+    public static TreePath findPathInNewTree(JTree tree, TreePath tp) {
+        TreePath root = tree.getPathForRow(0);
+        Object last = root.getLastPathComponent();
+        int pathIndex = 0;
+        if (!last.toString().equals(tp.getPathComponent(pathIndex).toString())) {
+            return null;
+        }
+        pathIndex++;
+        TreePath newPath = root;
+        if (tp.getPathCount() == 1) {
+            return newPath;
+        }
+        while (true) {
+            int c = tree.getModel().getChildCount(last);
+            boolean found = false;
+            for (int i = 0; i < c; i++) {
+                var child = tree.getModel().getChild(last, i);
+                if (child.toString().equals(tp.getPathComponent(pathIndex).toString())) {
+                    last = child;
+                    newPath = newPath.pathByAddingChild(last);
+                    pathIndex++;
+                    if (pathIndex == tp.getPathCount()) {
+                        return newPath;
+                    }
+                    found = true;
+                    break;
+                }
+            }
+            if (!found) {
+                return null;
+            }
+        }
+    }
 }