Fix update of proof tree in case of filter changes (fixes #3367)

key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java

@@ -78,22 +78,22 @@ public class ViewSettings extends AbstractPropertiesSettings {
     /**
      * Pretty Syntax is true by default, use Unicode symbols not
      */
-    private static final String PRETTY_SYNTAX = "PrettySyntax";
+    public static final String PRETTY_SYNTAX = "PrettySyntax";
 
     /**
      *
      */
-    private static final String USE_UNICODE = "UseUnicodeSymbols";
+    public static final String USE_UNICODE = "UseUnicodeSymbols";
 
     /**
      *
      */
-    private static final String SYNTAX_HIGHLIGHTING = "SyntaxHighlighting";
+    public static final String SYNTAX_HIGHLIGHTING = "SyntaxHighlighting";
 
     /**
      *
      */
-    private static final String HIDE_PACKAGE_PREFIX = "HidePackagePrefix";
+    public static final String HIDE_PACKAGE_PREFIX = "HidePackagePrefix";
 
     /**
      * confirm exiting by default

key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java

@@ -149,7 +149,7 @@ public synchronized void setSelectedSequentAndRuleApp(Node node, Sequent sequent
         selectedNode = node;
         selectedSequent = sequent;
         selectedRuleApp = ruleApp;
-        fireSelectedNodeChanged(node);
+        fireSelectedNodeChanged(previousNode);
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -829,8 +829,8 @@ public void unfreezeExceptAutoModeButton() {
     public void makePrettyView() {
         if (getMediator().ensureProofLoaded()) {
             getMediator().getNotationInfo().refresh(mediator.getServices());
-            getMediator().getSelectedProof().fireProofGoalsChanged();
         }
+        SwingUtilities.invokeLater(this::updateSequentView);
     }
 
     private void addToProofList(de.uka.ilkd.key.proof.ProofAggregate plist) {
@@ -1725,7 +1725,6 @@ public synchronized void selectedProofChanged(KeYSelectionEvent e) {
             }
 
             disableCurrentGoalView = false;
-            SwingUtilities.invokeLater(MainWindow.this::updateSequentView);
             makePrettyView();
         }
 
@@ -1791,5 +1790,4 @@ public void selectedNodeChanged(KeYSelectionEvent e) {
     public void setSequentView(SequentView sequentView) {
         sequentViewSearchBar.setSequentView(sequentView);
     }
-
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java

@@ -4,13 +4,14 @@
 package de.uka.ilkd.key.gui.actions;
 
 import java.awt.event.ActionEvent;
+import java.beans.PropertyChangeEvent;
 import java.beans.PropertyChangeListener;
-import java.util.EventObject;
 import javax.swing.*;
 
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import de.uka.ilkd.key.settings.ViewSettings;
 
 public final class HidePackagePrefixToggleAction extends MainWindowAction {
     public static final String NAME = "Hide Package Prefix";
@@ -36,7 +37,7 @@
         // removed, because there is only one
         // MainWindow!
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
-                .addPropertyChangeListener(viewSettingsListener);
+                .addPropertyChangeListener(ViewSettings.HIDE_PACKAGE_PREFIX, viewSettingsListener);
         updateSelectedState();
     }
 
@@ -55,16 +56,11 @@
                                                              // the UI will react on the settings
                                                              // change event!
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setHidePackagePrefix(selected);
-        updateMainWindow();
     }
 
-    private void updateMainWindow() {
-        mainWindow.makePrettyView();
-    }
-
-    private void handleViewSettingsChanged(EventObject e) {
+    protected void handleViewSettingsChanged(PropertyChangeEvent e) {
         updateSelectedState();
-        updateMainWindow();
+        mainWindow.makePrettyView();
     }
 
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java

@@ -5,13 +5,14 @@
 
 
 import java.awt.event.ActionEvent;
+import java.beans.PropertyChangeEvent;
 import java.beans.PropertyChangeListener;
-import java.util.EventObject;
-import javax.swing.JCheckBoxMenuItem;
+import javax.swing.*;
 
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import de.uka.ilkd.key.settings.ViewSettings;
 
 public class PrettyPrintToggleAction extends MainWindowAction {
     public static final String NAME = "Use Pretty Syntax";
@@ -25,9 +26,6 @@ public class PrettyPrintToggleAction extends MainWindowAction {
 
     /**
      * Listens for changes on {@code ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()}.
-     * <p>
-     * Such changes can occur in the Eclipse context when settings are changed in for instance the
-     * KeYIDE.
      */
     private final PropertyChangeListener viewSettingsListener = this::handleViewSettingsChanged;
 
@@ -39,7 +37,7 @@ public PrettyPrintToggleAction(MainWindow mainWindow) {
         // removed, because there is only one
         // MainWindow!
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
-                .addPropertyChangeListener(viewSettingsListener);
+                .addPropertyChangeListener(ViewSettings.PRETTY_SYNTAX, viewSettingsListener);
         updateSelectedState();
     }
 
@@ -48,7 +46,6 @@ protected void updateSelectedState() {
             ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isUsePretty();
         NotationInfo.DEFAULT_PRETTY_SYNTAX = prettySyntax;
         setSelected(prettySyntax);
-        // setSelected(NotationInfo.PRETTY_SYNTAX);
     }
 
     @Override
@@ -58,7 +55,6 @@ public void actionPerformed(ActionEvent e) {
         // will react on the settings change event!
         NotationInfo.DEFAULT_PRETTY_SYNTAX = selected;
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setUsePretty(selected);
-        updateMainWindow(selected);
     }
 
     protected void updateMainWindow(boolean prettySyntax) {
@@ -67,7 +63,7 @@ protected void updateMainWindow(boolean prettySyntax) {
         mainWindow.makePrettyView();
     }
 
-    protected void handleViewSettingsChanged(EventObject e) {
+    protected void handleViewSettingsChanged(PropertyChangeEvent e) {
         updateSelectedState();
         final boolean prettySyntax =
             ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isUsePretty();

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java

@@ -4,14 +4,24 @@
 package de.uka.ilkd.key.gui.actions;
 
 import java.awt.event.ActionEvent;
+import java.beans.PropertyChangeEvent;
+import java.beans.PropertyChangeListener;
 import javax.swing.JCheckBoxMenuItem;
 
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 
+import static de.uka.ilkd.key.settings.ViewSettings.SYNTAX_HIGHLIGHTING;
+
 public class SyntaxHighlightingToggleAction extends MainWindowAction {
     private static final long serialVersionUID = 6987252955535709994L;
 
+    /**
+     * Listens for changes on {@code ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()}.
+     */
+    private final PropertyChangeListener syntaxHighlightingListener =
+        this::handleViewSettingsChanged;
+
     public SyntaxHighlightingToggleAction(MainWindow window) {
         super(window);
         setName("Use Syntax Highlighting");
@@ -20,6 +30,11 @@ public SyntaxHighlightingToggleAction(MainWindow window) {
             + "slow down the rendering of longer ones.");
         final boolean useSyntaxHighlighting =
             ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isUseSyntaxHighlighting();
+        // Attention: The listener is never
+        // removed, because there is only one
+        // MainWindow!
+        ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
+                .addPropertyChangeListener(SYNTAX_HIGHLIGHTING, syntaxHighlightingListener);
         setSelected(useSyntaxHighlighting);
     }
 
@@ -28,7 +43,10 @@ public void actionPerformed(ActionEvent e) {
         boolean useSyntaxHighlighting = ((JCheckBoxMenuItem) e.getSource()).isSelected();
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
                 .setUseSyntaxHighlighting(useSyntaxHighlighting);
-        mainWindow.makePrettyView();
+        setSelected(useSyntaxHighlighting);
     }
 
+    protected void handleViewSettingsChanged(PropertyChangeEvent e) {
+        mainWindow.makePrettyView();
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java

@@ -4,13 +4,14 @@
 package de.uka.ilkd.key.gui.actions;
 
 import java.awt.event.ActionEvent;
+import java.beans.PropertyChangeEvent;
 import java.beans.PropertyChangeListener;
-import java.util.EventObject;
 import javax.swing.JCheckBoxMenuItem;
 
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
+import de.uka.ilkd.key.settings.ViewSettings;
 import de.uka.ilkd.key.util.UnicodeHelper;
 
 public class UnicodeToggleAction extends MainWindowAction {
@@ -38,7 +39,7 @@ public UnicodeToggleAction(MainWindow window) {
         // Attention: The listener is never// removed, because there is only one
         // MainWindow!
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings()
-                .addPropertyChangeListener(viewSettingsListener);
+                .addPropertyChangeListener(ViewSettings.USE_UNICODE, viewSettingsListener);
         updateSelectedState();
     }
 
@@ -64,14 +65,13 @@ public void actionPerformed(ActionEvent e) {
                                                                         // UI will react on the
                                                                         // settings change event!
         ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().setUseUnicode(useUnicode);
-        updateMainWindow();
     }
 
     protected void updateMainWindow() {
         mainWindow.makePrettyView();
     }
 
-    protected void handleViewSettingsChanged(EventObject e) {
+    protected void handleViewSettingsChanged(PropertyChangeEvent e) {
         updateSelectedState();
         updateMainWindow();
     }

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

@@ -2,49 +2,43 @@
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.gui.prooftree;
-/**
- * this class implements a TreeModel that can be displayed using the JTree class framework
- */
 
+import java.util.ArrayList;
 import javax.swing.tree.TreeNode;
 
 import de.uka.ilkd.key.proof.Node;
 
 import org.jspecify.annotations.NonNull;
 
+/**
+ * this class implements a TreeModel that can be displayed using the JTree class framework
+ */
 class GUIBranchNode extends GUIAbstractTreeNode implements TreeNode {
 
     private final Object label;
 
+    private ArrayList<TreeNode> childrenCache = null;
+
+
     public GUIBranchNode(GUIProofTreeModel tree, Node subTree, Object label) {
         super(tree, subTree);
         this.label = label;
     }
 
-
-    private TreeNode[] childrenCache = null;
-
-    private void createChildrenCache() {
-        childrenCache = new TreeNode[getChildCountHelp()];
-    }
-
     public TreeNode getChildAt(int childIndex) {
-        fillChildrenCache();
-        return childrenCache[childIndex];
-
+        ensureChildrenCacheExists();
+        return childrenCache.get(childIndex);
         /*
          * int count = 0; Node n = subTree; while ( childIndex != count && n.childrenCount() == 1 )
          * { count++; n = n.child(0); } if ( childIndex == count ) { return getProofTreeModel
          * ().getProofTreeNode(n); } else { return findBranch ( n.child(childIndex-count-1) ); }
          */
     }
 
-    private void fillChildrenCache() {
+    private void ensureChildrenCacheExists() {
         if (childrenCache == null) {
-            createChildrenCache();
-        }
-
-        if (childrenCache.length == 0 || childrenCache[0] != null) {
+            childrenCache = new ArrayList<>();
+        } else {
             return;
         }
 
@@ -56,7 +50,7 @@ private void fillChildrenCache() {
         }
 
         while (true) {
-            childrenCache[count] = getProofTreeModel().getProofTreeNode(n);
+            childrenCache.add(count, getProofTreeModel().getProofTreeNode(n));
             count++;
             final Node nextN = findChild(n);
             if (nextN == null) {
@@ -67,7 +61,7 @@ private void fillChildrenCache() {
 
         for (int i = 0; i != n.childrenCount(); ++i) {
             if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) {
-                childrenCache[count] = findBranch(n.child(i));
+                childrenCache.add(count, findBranch(n.child(i)));
                 count++;
             }
         }
@@ -86,38 +80,11 @@ public String getSearchString() {
 
     public int getChildCount() {
         if (childrenCache == null) {
-            createChildrenCache();
-        }
-        return childrenCache.length;
-    }
-
-    private int getChildCountHelp() {
-        int count = 0;
-        Node n = getNode();
-
-        if (n == null) {
-            return 0;
-        }
-
-        while (true) {
-            count++;
-            final Node nextN = findChild(n);
-            if (nextN == null) {
-                break;
-            }
-            n = nextN;
-        }
-
-        for (int i = 0; i != n.childrenCount(); ++i) {
-            if (!ProofTreeViewFilter.hiddenByGlobalFilters(n.child(i))) {
-                count++;
-            }
+            ensureChildrenCacheExists();
         }
-
-        return count;
+        return childrenCache.size();
     }
 
-
     public TreeNode getParent() {
         Node self = getNode();
         if (self == null) {