diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 09bcadfa5e2..506f3be7f77 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/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 diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java index cf18650a596..b3a72e3f867 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java +++ b/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); } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index c183cfe70a6..40cf80717b1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/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); } - } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java index d0a6c1dba29..ef96eaf8607 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java +++ b/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 @@ public HidePackagePrefixToggleAction(MainWindow mainWindow) { // removed, because there is only one // MainWindow! ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .addPropertyChangeListener(viewSettingsListener); + .addPropertyChangeListener(ViewSettings.HIDE_PACKAGE_PREFIX, viewSettingsListener); updateSelectedState(); } @@ -55,16 +56,11 @@ public void actionPerformed(ActionEvent e) { // 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(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java index 25a584fbaf5..357e31ac192 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java +++ b/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()}. - *

- * 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(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java index c0a62416777..03654fa2d1c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java +++ b/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(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java index 213a751ec8e..e5a3b0c1c45 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java +++ b/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(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java index bff237c9860..0aeac640d2f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIBranchNode.java @@ -2,36 +2,32 @@ * 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 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 @@ -39,12 +35,10 @@ public TreeNode getChildAt(int childIndex) { */ } - 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) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java index e2493edc282..6508c75a0f3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeModel.java @@ -17,7 +17,6 @@ import org.key_project.util.collection.ImmutableList; -import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -264,13 +263,17 @@ public boolean globalFilterActive() { */ public synchronized void setFilter(ProofTreeViewFilter filter, boolean active) { if (filter == null) { - activeNodeFilter = null; + if (activeNodeFilter != null) { + activeNodeFilter.setActive(false); + activeNodeFilter = null; + } updateTree((TreeNode) null); return; } if (!filter.global()) { - if (activeNodeFilter != null) + if (activeNodeFilter != null) { activeNodeFilter.setActive(false); + } activeNodeFilter = active ? (NodeFilter) filter : null; } filter.setActive(active); @@ -513,28 +516,6 @@ public GUIBranchNode getBranchNode(Node n, Object label) { } } - - /** stores exactly the paths that are expanded in the proof tree */ - private @NonNull Collection expansionState = Collections.emptySet(); - - public void setExpansionState(@NonNull Collection c) { - expansionState = c; - } - - public @NonNull Collection getExpansionState() { - return expansionState; - } - - TreePath selection; - - public void storeSelection(TreePath t) { - selection = t; - } - - public TreePath getSelection() { - return selection; - } - public NodeFilter getActiveNodeFilter() { return activeNodeFilter; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index c12df26cb5c..ac7fcd07994 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -300,7 +300,11 @@ public void actionPerformed(ActionEvent e) { } } if (sibling instanceof GUIBranchNode) { - context.proofTreeView.selectBranchNode((GUIBranchNode) sibling); + var tp = context.proofTreeView.selectBranchNode((GUIBranchNode) sibling); + if (tp != null) { + context.delegateView.setSelectionPath(tp); + context.delegateView.scrollPathToVisible(tp); + } } } } @@ -333,7 +337,11 @@ public void actionPerformed(ActionEvent e) { } } if (sibling instanceof GUIBranchNode) { - context.proofTreeView.selectBranchNode((GUIBranchNode) sibling); + var tp = context.proofTreeView.selectBranchNode((GUIBranchNode) sibling); + if (tp != null) { + context.delegateView.setSelectionPath(tp); + context.delegateView.scrollPathToVisible(tp); + } } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java index 17035b07d7e..f90def1f60d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSearchBar.java @@ -71,11 +71,12 @@ private synchronized boolean search(String searchString, Position.Bias direction tp = new TreePath(node.getPath()); } if (node instanceof GUIBranchNode) { - this.proofTreeView.selectBranchNode((GUIBranchNode) node); - } else { - this.proofTreeView.delegateView.scrollPathToVisible(tp); - this.proofTreeView.delegateView.setSelectionPath(tp); + tp = this.proofTreeView.selectBranchNode((GUIBranchNode) node); } + + this.proofTreeView.delegateView.scrollPathToVisible(tp); + this.proofTreeView.delegateView.setSelectionPath(tp); + return currentRow != -1; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 8de525bfccb..d0361823e12 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -102,13 +102,9 @@ public class ProofTreeView extends JPanel implements TabPanel { private KeYMediator mediator; /** - * Stores for each loaded proof the GUI tree model. + * Stores for each loaded proof the view state */ - private final WeakHashMap models = new WeakHashMap<>(20); - /** - * Stores for each loaded proof the position of the scroll view. - */ - private final WeakHashMap scrollState = new WeakHashMap<>(); + private final WeakHashMap viewStates = new WeakHashMap<>(20); /** * The (currently selected) proof this view shows. @@ -407,8 +403,8 @@ public boolean selectAbove() { int row = delegateView.getRowForPath(path); row--; while (delegateView.getPathForRow(row) != null) { - TreePath tp = delegateView.getPathForRow(row); - var treeNode = (GUIAbstractTreeNode) tp.getLastPathComponent(); + final TreePath tp = delegateView.getPathForRow(row); + final var treeNode = (GUIAbstractTreeNode) tp.getLastPathComponent(); if (treeNode instanceof GUIBranchNode && treeNode.getNode().parent() != null && treeNode.getNode().parent().childrenCount() > 1 && !delegateView.isExpanded(tp)) { @@ -463,37 +459,47 @@ public boolean selectBelow() { * @param p the Proof that has been loaded */ private void setProof(Proof p) { - if (proof != null) { - // save old scroll height - JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent(); - scrollState.put(proof, scroller.getVerticalScrollBar().getValue()); - } if (proof == p) { return; // proof is already loaded } - ProofTreeViewFilter.NodeFilter filter = null; - if (delegateModel != null) { - filter = delegateModel.getActiveNodeFilter(); - expansionState.disconnect(); - delegateModel.setExpansionState(expansionState.copyState()); - delegateModel.storeSelection(delegateView.getSelectionPath()); - delegateModel.unregister(); - delegateModel.removeTreeModelListener(proofTreeSearchPanel); + + ProofTreeViewFilter.NodeFilter previousNodeFilter = null; + boolean previousNodeFilterState = false; + if (proof != null) { + // save old view state + if (delegateModel != null) { // is it ever not null when proof != null? + JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent(); + expansionState.disconnect(); + previousNodeFilter = delegateModel.getActiveNodeFilter(); + previousNodeFilterState = + previousNodeFilter != null && previousNodeFilter.isActive(); + ProofTreeViewState memorizeProofTreeViewState = new ProofTreeViewState( + delegateModel, + expansionState.copyState(), + delegateView.getSelectionPath(), + scroller.getVerticalScrollBar().getValue()); + viewStates.put(proof, memorizeProofTreeViewState); + delegateModel.unregister(); + delegateModel.removeTreeModelListener(proofTreeSearchPanel); + } } proof = p; if (proof != null) { - delegateModel = models.get(p); - if (delegateModel == null) { - delegateModel = new GUIProofTreeModel(p); - models.put(p, delegateModel); + ProofTreeViewState memorizedState = viewStates.get(proof); + + if (memorizedState == null) { + memorizedState = new ProofTreeViewState(new GUIProofTreeModel(proof), + Collections.emptyList(), null, 0); } + + delegateModel = memorizedState.model; delegateModel.addTreeModelListener(proofTreeSearchPanel); delegateModel.register(); delegateView.setModel(delegateModel); expansionState = - new ProofTreeExpansionState(delegateView, delegateModel.getExpansionState()); + new ProofTreeExpansionState(delegateView, memorizedState.expansionState); delegateView.expandRow(0); // Save expansion state to restore: @@ -505,18 +511,18 @@ private void setProof(Proof p) { } Collections.sort(rowsToExpand); - // Redraw the tree in case the ProofTreeViewFilters have changed - // since the last time the proof was loaded. - delegateModel.setFilter(filter, filter != null && filter.isActive()); - - // Expand previously visible rows. - for (int i : rowsToExpand) { - delegateView.expandRow(i); + // restore filters + for (var viewFilter : ProofTreeViewFilter.ALL) { + setFilter(viewFilter, viewFilter.isActive()); } - if (delegateModel.getSelection() != null) { - delegateView.setSelectionPath(delegateModel.getSelection()); - delegateView.scrollPathToVisible(delegateModel.getSelection()); + // restore node filter + delegateModel.setFilter(previousNodeFilter, previousNodeFilterState); + + // restore selection + if (memorizedState.selectionPath != null) { + delegateView.setSelectionPath(memorizedState.selectionPath); + delegateView.scrollPathToVisible(memorizedState.selectionPath); } else { if (mediator.getSelectedProof() == p && mediator.getSelectedNode() != null) { makeNodeVisible(mediator.getSelectedNode()); @@ -526,11 +532,16 @@ private void setProof(Proof p) { } } + // Expand previously visible rows. + for (int i : rowsToExpand) { + delegateView.expandRow(i); + } + // Restore previous scroll position. JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent(); - Integer i = scrollState.get(proof); - if (i != null) { - scroller.getVerticalScrollBar().setValue(i); + Integer scrollState = memorizedState.scrollState; + if (scrollState != null) { + scroller.getVerticalScrollBar().setValue(scrollState); } } else { delegateModel = null; @@ -539,18 +550,11 @@ private void setProof(Proof p) { expansionState = null; } proofTreeSearchPanel.reset(); - - for (ProofTreeViewFilter f : ProofTreeViewFilter.ALL) { - if (f.isActive()) { - setFilter(f, true); - } - } } public void removeProofs(Proof[] ps) { for (final Proof p : ps) { - models.remove(p); - scrollState.remove(p); + viewStates.remove(p); mediator.getCurrentlyOpenedProofs().remove(p); } } @@ -562,13 +566,29 @@ public void makeNodeVisible(Node n) { if (n == null) { return; } - final GUIAbstractTreeNode node = delegateModel.getProofTreeNode(n); if (node == null) { return; } TreeNode[] obs = node.getPath(); + + if (n.sequent() != mediator.getSelectionModel().getSelectedSequent()) { + // in this case we have to select a child of an OSS node + ArrayList pathToOSSChild = new ArrayList<>(); + pathToOSSChild.addAll(Arrays.asList(obs)); + for (int i = 0; i < node.getChildCount(); i++) { + if (node.getChildAt(i) instanceof GUIOneStepChildTreeNode ossChild) { + if (ossChild.getRuleApp() == mediator.getSelectionModel() + .getSelectedRuleApp()) { + pathToOSSChild.add(ossChild); + break; + } + } + } + obs = pathToOSSChild.toArray(new TreeNode[0]); + } + TreePath tp = new TreePath(obs); treeSelectionListener.ignoreChange = true; delegateView.getSelectionModel().setSelectionPath(tp); @@ -601,7 +621,7 @@ private void collapseClosedNodesHelp(TreePath path) { Object node = path.getLastPathComponent(); - if (node instanceof GUIBranchNode && ((GUIBranchNode) node).getNode().isClosed()) { + if (node instanceof GUIBranchNode branchNode && branchNode.getNode().isClosed()) { delegateView.collapsePath(path); return; } @@ -645,22 +665,14 @@ private void collapseOthersHelp(TreePath start, TreePath stop) { * Selects the given Branchnode in the ProofTreeView and displays the first child in the main * view. */ - void selectBranchNode(GUIBranchNode node) { + TreePath selectBranchNode(GUIBranchNode node) { if (node == null) { - return; + return null; } proofListener.ignoreNodeSelectionChange = true; mediator.getSelectionModel().setSelectedNode(node.getNode()); proofListener.ignoreNodeSelectionChange = false; - TreePath tp = new TreePath(node.getPath()); - treeSelectionListener.ignoreChange = true; - delegateView.getSelectionModel().setSelectionPath(tp); - delegateView.scrollPathToVisible(tp); - delegateView.validate(); - treeSelectionListener.ignoreChange = false; - - delegateModel.storeSelection(delegateView.getSelectionPath()); - + return new TreePath(node.getPath()); } public void showSearchPanel() { @@ -689,7 +701,8 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) { return false; } - final TreePath selectedPath = delegateModel.getSelection(); + TreePath selectedPath = delegateView.getSelectionPath(); + if (selectedPath == null) { return false; } @@ -697,84 +710,72 @@ public boolean setFilter(ProofTreeViewFilter filter, boolean selected) { // Save expansion state to restore. List rowsToExpand = new ArrayList<>(expansionState); - final TreePath branch; final Node invokedNode; - if (selectedPath.getLastPathComponent() instanceof GUIProofTreeNode) { + + final var lastPathComponent = selectedPath.getLastPathComponent(); + if (lastPathComponent instanceof GUIProofTreeNode guiNode) { branch = selectedPath.getParentPath(); - invokedNode = - ((GUIProofTreeNode) selectedPath.getLastPathComponent()).getNode(); + invokedNode = guiNode.getNode(); } else { branch = selectedPath; - invokedNode = ((GUIBranchNode) selectedPath.getLastPathComponent()).getNode(); + invokedNode = ((GUIAbstractTreeNode) lastPathComponent).getNode(); } - if (!filter.global()) { - delegateModel.setFilter(filter, selected); - if (branch == selectedPath) { - if (delegateModel.getRoot() instanceof GUIBranchNode) { - TreeNode node = ((GUIAbstractTreeNode) delegateModel.getRoot()) - .findBranch(invokedNode); - if (node instanceof GUIBranchNode) { - selectBranchNode((GUIBranchNode) node); - } - } - } else { - delegateView.scrollPathToVisible(selectedPath); - delegateView.setSelectionPath(selectedPath); - } + delegateModel.setFilter(filter, selected); + + if (!filter.global() && branch == selectedPath) { + selectedPath = getPathForBranchNode(invokedNode, selectedPath); + } else if (branch == selectedPath && + (!selected || invokedNode.parent() == null || + delegateModel + .getProofTreeNode(invokedNode.parent()) + .findChild(invokedNode.parent()) == null)) { + selectedPath = getPathForBranchNode(invokedNode, selectedPath); } else { - delegateModel.setFilter(filter, selected); - if (branch == selectedPath) { - if (!selected) { - if (delegateModel.getRoot() instanceof GUIBranchNode) { - TreeNode node = ((GUIAbstractTreeNode) delegateModel.getRoot()) - .findBranch(invokedNode); - if (node instanceof GUIBranchNode) { - selectBranchNode((GUIBranchNode) node); - } - } - } else { - if (invokedNode.parent() == null || delegateModel - .getProofTreeNode(invokedNode.parent()) - .findChild(invokedNode.parent()) == null) { - // it's still a branch - if (delegateModel.getRoot() instanceof GUIBranchNode) { - TreeNode node = - ((GUIAbstractTreeNode) delegateModel.getRoot()) - .findBranch(invokedNode); - if (node instanceof GUIBranchNode) { - selectBranchNode((GUIBranchNode) node); - } - } - } else { - TreePath tp = new TreePath(delegateModel - .getProofTreeNode(invokedNode).getPath()); - delegateView.scrollPathToVisible(tp); - delegateView.setSelectionPath(tp); - } - } - } else { - TreePath tp = new TreePath( - delegateModel.getProofTreeNode(invokedNode).getPath()); - delegateView.scrollPathToVisible(tp); - delegateView.setSelectionPath(tp); + selectedPath = new TreePath(delegateModel.getProofTreeNode(invokedNode).getPath()); + if (lastPathComponent instanceof GUIOneStepChildTreeNode) { + selectedPath = selectedPath.pathByAddingChild(lastPathComponent); } } + delegateView.setSelectionPath(selectedPath); + delegateView.scrollPathToVisible(selectedPath); + // Expand previously visible rows. for (TreePath tp : rowsToExpand) { TreePath newTp = delegateView.getPathForRow(0); for (int i = 1; i < tp.getPathCount(); i++) { - Node n = ((GUIBranchNode) tp.getPathComponent(i)).getNode(); - newTp = newTp.pathByAddingChild( - delegateModel.getBranchNode(n, n.getNodeInfo().getBranchLabel())); + if (tp.getPathComponent(i) instanceof GUIBranchNode pathComp) { + final Node n = pathComp.getNode(); + newTp = newTp.pathByAddingChild( + delegateModel.getBranchNode(n, n.getNodeInfo().getBranchLabel())); + } } delegateView.expandPath(newTp); } return true; } + /** + * if invoked node is modelled as branch node, select the branch node + * + * @param invokedNode the selected node in the proof + * @param defaultPath the {@link TreePath} to be returned if the invokedNode does not have an + * associated branch node + * @return the path to the branch node if available otherwise {@code defaultPath} + */ + private TreePath getPathForBranchNode(Node invokedNode, TreePath defaultPath) { + if (delegateModel.getRoot() instanceof GUIBranchNode rootNode) { + final TreeNode node = rootNode.findBranch(invokedNode); + if (node instanceof GUIBranchNode childAsBranchNode && + !(defaultPath.getLastPathComponent() instanceof GUIOneStepChildTreeNode)) { + return selectBranchNode(childAsBranchNode); + } + } + return defaultPath; + } + @NonNull @Override public Collection getTitleCActions() { @@ -941,15 +942,14 @@ public void valueChanged(TreeSelectionEvent e) { } TreePath newTP = e.getNewLeadSelectionPath(); - delegateModel.storeSelection(newTP); - if (treeNode.getNode().proof().isDisposed()) { setProof(null); return; } + if (treeNode instanceof GUIBranchNode) { - selectBranchNode((GUIBranchNode) treeNode); + newTP = selectBranchNode((GUIBranchNode) treeNode); } else { Node node = treeNode.getNode(); Goal selected = proof.getOpenGoal(node); @@ -965,15 +965,16 @@ public void valueChanged(TreeSelectionEvent e) { .replaceFormula(ossNode.getFormulaNr(), pio.sequentFormula()).sequent(); mediator.getSelectionModel().setSelectedSequentAndRuleApp( ossParentNode.getNode(), modifiedSequent, ossNode.getRuleApp()); - - // ensure the proper node is selected in the tree - ignoreChange = true; - delegateView.setSelectionPath(newTP); - ignoreChange = false; } else { mediator.nonGoalNodeChosen(node); } } + // ensure the proper node is selected in the tree + if (newTP != null && !newTP.equals(e.getNewLeadSelectionPath())) { + ignoreChange = true; + delegateView.setSelectionPath(newTP); + ignoreChange = false; + } } } @@ -1286,4 +1287,20 @@ public Node getSelectedNode() { ? ((GUIAbstractTreeNode) treeNode).getNode() : null; } + + /** + * Record used to store the state of the proof tree view for a particular proof such that it can + * be stored and + * restored when switching proofs + * + * @param model the {@link GUIProofTreeModel} of the proof + * @param expansionState the expanded tree paths + * @param selectionPath the path to the currently selected node + * @param scrollState the state of the scroll pane + */ + record ProofTreeViewState(GUIProofTreeModel model, + Collection expansionState, + TreePath selectionPath, + Integer scrollState) { + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java b/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java index f66f262519f..1f4e9b91330 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java @@ -143,7 +143,9 @@ protected void done() { mediator.getUI().reportStatus(this, errorMessage); } fireTaskFinished(runTime, message); - mediator.getSelectionModel().defaultSelection(); + if (mediator.getSelectedProof() != null) { + mediator.getSelectionModel().defaultSelection(); + } } } };