Skip to content

Commit

Permalink
USe refactorings from #3369 but preserve non-local filter semantics f…
Browse files Browse the repository at this point in the history 
…or proof tree view
  • Loading branch information
@unp1
unp1 committed Dec 2, 2023
1 parent ce27480 commit c899372
Showing 1 changed file with 26 additions and 55 deletions.
81 changes: 26 additions & 55 deletions key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@
import de.uka.ilkd.key.proof.reference.ClosedBy;
import de.uka.ilkd.key.rule.RuleApp;
import de.uka.ilkd.key.settings.ProofIndependentSettings;
import de.uka.ilkd.key.util.Pair;
import de.uka.ilkd.key.util.ThreadUtilities;

import org.key_project.util.collection.ImmutableList;
Expand Down Expand Up @@ -404,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)) {
Expand Down Expand Up @@ -464,35 +463,22 @@ private void setProof(Proof p) {
return; // proof is already loaded
}

ProofTreeViewFilter.NodeFilter previousNodeFilter = null;
boolean previousNodeFilterState = false;
if (proof != null) {
// save old view state
JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent();
if (delegateModel != null) { // is it ever not null when proof != null?
var nodeFilter = delegateModel.getActiveNodeFilter();
JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent();
expansionState.disconnect();

final HashSet<ProofTreeViewFilter> activeFilters = new HashSet<>();
for (ProofTreeViewFilter f : ProofTreeViewFilter.ALL) {
if (f.isActive()) {
// ignore node filters as only one might be active at a given time
// their state is saved independently
activeFilters.add(f);
}
}

previousNodeFilter = delegateModel.getActiveNodeFilter();
previousNodeFilterState =
previousNodeFilter != null && previousNodeFilter.isActive();
ProofTreeViewState memorizeProofTreeViewState = new ProofTreeViewState(
delegateModel,
expansionState.copyState(),
delegateView.getSelectionPath(),
activeFilters,
new Pair<>(nodeFilter, nodeFilter != null && nodeFilter.isActive()),
scroller.getVerticalScrollBar().getValue());

viewStates.put(proof, memorizeProofTreeViewState);

if (nodeFilter != null) {
delegateModel.setFilter(nodeFilter, false);
}
delegateModel.unregister();
delegateModel.removeTreeModelListener(proofTreeSearchPanel);
}
Expand All @@ -504,9 +490,8 @@ private void setProof(Proof p) {
ProofTreeViewState memorizedState = viewStates.get(proof);

if (memorizedState == null) {
memorizedState = new ProofTreeViewState(new GUIProofTreeModel(p),
Collections.emptyList(), null, new HashSet<>(),
new Pair<>(null, false), 0);
memorizedState = new ProofTreeViewState(new GUIProofTreeModel(proof),
Collections.emptyList(), null, 0);
}

delegateModel = memorizedState.model;
Expand All @@ -526,35 +511,15 @@ private void setProof(Proof p) {
}
Collections.sort(rowsToExpand);

// Restore previous scroll position.
JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent();
Integer scrollState = memorizedState.scrollState;
if (scrollState != null) {
scroller.getVerticalScrollBar().setValue(scrollState);
}

// this selection must happen before and later after restoring the filters
// as setting a filter immediately applies it and
if (memorizedState.selectionPath != null) {
delegateView.setSelectionPath(memorizedState.selectionPath);
} else {
delegateView.setSelectionRow(0);
}

// restore filters
for (var viewFilter : ProofTreeViewFilter.ALL) {
setFilter(viewFilter,
memorizedState.activeFilters.contains(viewFilter));
setFilter(viewFilter, viewFilter.isActive());
}

delegateModel.setFilter(memorizedState.nodeFilterState.first,
memorizedState.nodeFilterState.second);

// Expand previously visible rows.
for (int i : rowsToExpand) {
delegateView.expandRow(i);
}
// restore node filter
delegateModel.setFilter(previousNodeFilter, previousNodeFilterState);

// restore selection
if (memorizedState.selectionPath != null) {
delegateView.setSelectionPath(memorizedState.selectionPath);
delegateView.scrollPathToVisible(memorizedState.selectionPath);
Expand All @@ -566,6 +531,18 @@ private void setProof(Proof p) {
delegateView.setSelectionRow(1);
}
}

// Expand previously visible rows.
for (int i : rowsToExpand) {
delegateView.expandRow(i);
}

// Restore previous scroll position.
JScrollPane scroller = (JScrollPane) delegateView.getParent().getParent();
Integer scrollState = memorizedState.scrollState;
if (scrollState != null) {
scroller.getVerticalScrollBar().setValue(scrollState);
}
} else {
delegateModel = null;
delegateView
Expand All @@ -589,7 +566,6 @@ public void makeNodeVisible(Node n) {
if (n == null) {
return;
}

final GUIAbstractTreeNode node = delegateModel.getProofTreeNode(n);
if (node == null) {
return;
Expand Down Expand Up @@ -1286,7 +1262,6 @@ public Node getSelectedNode() {
: null;
}


/**
* Record used to store the state of the proof tree view for a particular proof such that it can
* be stored and
Expand All @@ -1295,15 +1270,11 @@ public Node getSelectedNode() {
* @param model the {@link GUIProofTreeModel} of the proof
* @param expansionState the expanded tree paths
* @param selectionPath the path to the currently selected node
* @param activeFilters the activated {@link ProofTreeViewFilter}s
* @param nodeFilterState the activated (if any) {@link ProofTreeViewFilter.NodeFilter}
* @param scrollState the state of the scroll pane
*/
record ProofTreeViewState(GUIProofTreeModel model,
Collection<TreePath> expansionState,
TreePath selectionPath,
HashSet<ProofTreeViewFilter> activeFilters,
Pair<ProofTreeViewFilter.NodeFilter, Boolean> nodeFilterState,
Integer scrollState) {
}
}

0 comments on commit c899372

Please sign in to comment.