option menu: when search filter doesn't have results, ignore it and show an effect on the filter text

This commit is contained in:
yugecin
2017-05-28 19:30:41 +02:00
parent 6d3336b7ea
commit 70737e4472
2 changed files with 73 additions and 5 deletions

View File

@@ -78,6 +78,10 @@ public class Option {
return filtered;
}
public void setFiltered(boolean flag) {
this.filtered = flag;
}
/**
* Check if this option should be filtered (= not shown) because it does not
* match the search string.