manifest: wait 200 ms of inactivity before applying manifest file filter
This improves the performance of the manifest filter when the number of files is large.
Up until now the manifest file list was filtered each time that the user typed a key on the filter box. If the user typed 5 characters on the filter box the manifest file list would be filtered five times (once with the first character, once with the first two characters, etc). When the number of files is large, each filter operation can take longer than the time it takes for the user to input a new character. The result is that the filter requests can pile pile up and the filter box cann seem unresponsive.
This patch improves the situation by not triggering the filtering immediately. Instead, each time a key is pressed on the filter box a filtering operation is scheduled 200 ms in the future. If the user modifies the file filter box before the actual filtering operation starts the previous scheduled filtering operation is aborted, and a new one is scheduled 200 ms in the future.
The result is that if the user types several keys while a filter operation is being performed, only the last filter operation will be executed.