Skip to content

Commit

Permalink
Minor clean up and refactoring
Browse files Browse the repository at this point in the history
  • Loading branch information
unp1 committed Dec 2, 2023
1 parent ce27480 commit f0c7433
Showing 1 changed file with 38 additions and 39 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -471,22 +471,13 @@ private void setProof(Proof p) {
var nodeFilter = delegateModel.getActiveNodeFilter();
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);
}
}

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

viewStates.put(proof, memorizeProofTreeViewState);

Expand Down Expand Up @@ -526,35 +517,17 @@ 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));
memorizedState.activeFilters.contains(viewFilter));
}

// restore node filter
delegateModel.setFilter(memorizedState.nodeFilterState.first,
memorizedState.nodeFilterState.second);

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

// restore selection
if (memorizedState.selectionPath != null) {
delegateView.setSelectionPath(memorizedState.selectionPath);
delegateView.scrollPathToVisible(memorizedState.selectionPath);
Expand All @@ -566,6 +539,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 @@ -575,6 +560,20 @@ private void setProof(Proof p) {
proofTreeSearchPanel.reset();
}

/**
* retrieves the activated filters
* @return collection of all activated filters
*/
private Set<ProofTreeViewFilter> getActiveFilters() {
final HashSet<ProofTreeViewFilter> activeFilters = new HashSet<>();
for (ProofTreeViewFilter f : ProofTreeViewFilter.ALL) {
if (f.isActive()) {
activeFilters.add(f);
}
}
return activeFilters;
}

public void removeProofs(Proof[] ps) {
for (final Proof p : ps) {
viewStates.remove(p);
Expand Down Expand Up @@ -1302,7 +1301,7 @@ public Node getSelectedNode() {
record ProofTreeViewState(GUIProofTreeModel model,
Collection<TreePath> expansionState,
TreePath selectionPath,
HashSet<ProofTreeViewFilter> activeFilters,
Collection<ProofTreeViewFilter> activeFilters,
Pair<ProofTreeViewFilter.NodeFilter, Boolean> nodeFilterState,
Integer scrollState) {
}
Expand Down

0 comments on commit f0c7433

Please sign in to comment.