Okay, here is an experimental version with this functionality (and a bit of code cleanup):
"Filter by player names or handles, current map, mode or mutators, server description, IP address or port."
I have also experimented with color highlighting of matched patterns, but scrapped that because
* it is a mess with case insensitive matches
* the modes, maps and (especially!) the playernames are already busy with color
* I gotta be careful not to create garbage when replacing strings at will
Another cool note: I realize quin made some layout fixes, including that the frame size remains the same when only few servers are shown. That's nice.
I guess I'll make another pull request after some more careful testing.
EDIT: Thanks for merging! For details, see