Render filtered results piecemally. Disable filter button while filtering is ongoing. Clear selection before filtering. GitHub issue #88

auto-update
Zlatin Balevsky 2021-10-16 14:58:07 +01:00
parent f688a0bcb4
commit b501bc0f5f
No known key found for this signature in database
GPG Key ID: A72832072D525E41
2 changed files with 14 additions and 2 deletions

View File

@ -65,12 +65,15 @@ class BrowseModel {
}
void filterResults() {
filterer?.cancel()
results.clear()
root.removeAllChildren()
filterer?.cancel()
view.clearForFilter()
view.refreshResults()
if (filter != null) {
filterer = new Filterer()
filterer.execute()
setFilterEnabled(false)
} else {
synchronized (allResults) {
results.addAll(allResults)
@ -103,11 +106,13 @@ class BrowseModel {
@Override
protected void process(List<UIResultEvent> chunks) {
if (cancelled)
if (cancelled || chunks.isEmpty())
return
results.addAll(chunks)
for (UIResultEvent result : chunks)
resultsTreeModel.addToTree(result)
view.refreshResults()
view.expandUnconditionally()
}
@Override
@ -116,6 +121,7 @@ class BrowseModel {
return
view.refreshResults()
view.expandUnconditionally()
setFilterEnabled(true)
}
}
}

View File

@ -296,6 +296,12 @@ class BrowseView {
showTree.call()
}
void clearForFilter() {
resultsTable.clearSelection()
treeExpansions.manualExpansion = false
treeExpansions.expandedPaths.clear()
}
void refreshResults() {
int [] selectedRows = resultsTable.getSelectedRows()
if (lastSortEvent != null) {